arrowCongr_refl — Mathlib

English

For any R-algebras A1, A2, the transported identity along the identity isomorphisms equals the identity on the algebra homs: arrowCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A1 →ₐ[R] A2).

Русский

Для произвольных R-алгебр A1, A2 перенесение по тождественному эквивалентному отображению совпадает с тождественным отображением на типе алгебраических гомоморфизмов.

LaTeX

$$$\\operatorname{arrowCongr}(\\mathrm{refl},\\mathrm{refl}) = \\mathrm{refl}_{(A_1 \\to\\!_R A_2)}$$$

Lean4

@[simp]
theorem arrowCongr_refl : arrowCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A₁ →ₐ[R] A₂) :=
  rfl

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