symm_mk — Mathlib

English

The reflexive algebra equivalence corresponds to the identity RingHom on the underlying algebra.

Русский

Рефлексивная алгебраическая эквивалентность соответствует тождественному RingHom на базовой алгебре.

LaTeX

$$$ refl_toRingHom: (refl : A_1 \simeq_{R} A_1) = RingHom.id A_1 $$$

Lean4

@[simp]
theorem symm_mk (f f') (h₁ h₂ h₃ h₄ h₅) :
    (⟨⟨f, f', h₁, h₂⟩, h₃, h₄, h₅⟩ : A₁ ≃ₐ[R] A₂).symm =
      { symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ with
        toFun := f'
        invFun := f } :=
  rfl

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