symm_toRingHom_comp_toRingHom — Mathlib

English

The composition of e.symm.toRingHom with e.toRingHom is the identity on R: e.symm.toRingHom ∘ e.toRingHom = id_R.

Русский

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

LaTeX

$$$ e.symm.toRingHom \circ e.toRingHom = RingHom.id _ $$$

Lean4

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

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