symm_toNonUnitalRingHom_comp_toNonUnitalRingHom

English

The composition of e.symm.toNonUnitalRingHom with e.toNonUnitalRingHom equals the identity on R.

Русский

Состав e.symm.toNonUnitalRingHom и e.toNonUnitalRingHom равен тождественному на R.

LaTeX

$$$$ e.symm.toNonUnitalRingHom .\\circ e.toNonUnitalRingHom = \\mathrm{id}_{R}. $$$$

Lean4

@[simp]
theorem symm_toNonUnitalRingHom_comp_toNonUnitalRingHom (e : R ≃+* S) :
    e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id _ :=
  by
  ext
  simp

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