toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply

English

For all y in S, e.toNonUnitalRingHom (e.symm.toNonUnitalRingHom y) = y.

Русский

Для всех y в S выполняется e.toNonUnitalRingHom( e.symm.toNonUnitalRingHom y ) = y.

LaTeX

$$$$ \\forall y:\\, S,\\; e^{\\text{toNonUnitalRingHom}}(e^{\\text{symm}}(y)) = y. $$$$

Lean4

@[simp]
theorem toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply (e : R ≃+* S) :
    ∀ y : S, e.toNonUnitalRingHom (e.symm.toNonUnitalRingHom y) = y :=
  e.toEquiv.apply_symm_apply

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