ofAlgHom_coe_algHom — Mathlib

English

The equivalence induced by refl on both sides is the identity equivalence on the space of algebra equivalences.

Русский

Эквивалентность, полученная из тождественного преобразования слева и справа, совпадает с тождественным отображением на пространстве алгебраических эквивалентностей.

LaTeX

$$$\\operatorname{equivCongr}(\\mathrm{refl},\\mathrm{refl}) = \\mathrm{Equiv.refl} (A_1 ≃ₐ[R] A_2')$$$

Lean4

@[simp]
theorem ofAlgHom_coe_algHom (f : A₁ ≃ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) : ofAlgHom (↑f) g h₁ h₂ = f :=
  ext fun _ => rfl

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