toRingHom_comp_symm_toRingHom — Mathlib

English

The composition of e.toRingHom with e.symm.toRingHom is the identity on S: e.toRingHom ∘ e.symm.toRingHom = id_S.

Русский

Состав e.toRingHom и e.symm.toRingHom равен тождественному отображению на S: e.toRingHom ∘ e.symm.toRingHom = id_S.

LaTeX

$$$ e.toRingHom \circ e.symm.toRingHom = RingHom.id_S $$$

Lean4

theorem toRingHom_comp_symm_toRingHom (e : R ≃+* S) : e.toRingHom.comp e.symm.toRingHom = RingHom.id _ := by simp

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