symm_comp — Mathlib

English

Similarly, composing the inverse with the forward map yields the identity on the domain.

Русский

Аналогично: композиция обратного и прямого отображения дает тождество на домене.

LaTeX

$$$$ (e.symm : S \\to+* R).\\text{comp}(e : R \\to+* S) = \\text{RingHom.id } R. $$$$

Lean4

@[simp]
theorem symm_comp (e : R ≃+* S) : (e.symm : S →+* R).comp (e : R →+* S) = RingHom.id R :=
  RingHom.ext e.symm_apply_apply

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