symm_toEquiv_eq_symm

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.symm_toEquiv_eq_symm

English

The coe of the reflexive algebra equivalence equals the identity map.

Русский

Коэрция рефлексивной эквивалентности совпадает с тождественным отображением.

LaTeX

$$$ \text{coe}_{\mathrm{refl}} = \mathrm{id} $$$

Lean4

/-- `simp` normal form of `invFun_eq_symm` -/
@[simp]
theorem symm_toEquiv_eq_symm {e : A₁ ≃ₐ[R] A₂} : (e : A₁ ≃ A₂).symm = e.symm :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru