toRingEquiv_symm — Mathlib

English

For any endomorphism e of an algebra A, the underlying ring isomorphism has as inverse the underlying map of the inverse algebra equivalence; i.e. the inverse of the ring isomorphism induced by e is the ring isomorphism induced by e.symm.

Русский

Для любой эндоморфной алгебраической эквивалентности e на A обратный кольцевой изоморфизм совпадает с изоморфизмом, полученным от e.symm.

LaTeX

$$$(e : A \to A)^{-1} = e^{-1}$$$

Lean4

theorem toRingEquiv_symm (f : A₁ ≃ₐ[R] A₁) : (f : A₁ ≃+* A₁).symm = f.symm :=
  rfl

Похожие утверждения