congr_refl — Mathlib

English

The congruence map respects the identity isomorphisms: congr(id, id) is the identity isomorphism.

Русский

Конгруэнция идёт в соответствие с тождественными изоморфизмами: congr(id, id) — тождественный изоморфизм.

LaTeX

$$congr(AlgEquiv.refl, AlgEquiv.refl) = AlgEquiv.refl$$

Lean4

@[simp]
theorem congr_refl : congr (.refl : A ≃ₐ[S] A) (.refl : B ≃ₐ[R] B) = .refl :=
  AlgEquiv.coe_algHom_injective <| map_id

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