toRingHom_apply_symm_toRingHom_apply

English

For any ring isomorphism e: R ≃+* S, and for every y ∈ S, the composition of the forward ring hom with the inverse ring hom equals y: e.toRingHom (e.symm.toRingHom y) = y.

Русский

Пусть e: R ≃+* S — изоморфизм колец. Для любого y ∈ S выполняется, что e.toRingHom (e.symm.toRingHom y) = y.

LaTeX

$$$ \forall y \in S,\ e.toRingHom (e.symm.toRingHom y) = y $$$

Lean4

theorem toRingHom_apply_symm_toRingHom_apply (e : R ≃+* S) : ∀ y : S, e.toRingHom (e.symm.toRingHom y) = y :=
  e.toEquiv.apply_symm_apply

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