symm_toRingHom_apply_toRingHom_apply

English

For any ring equivalence e, and every x ∈ R, applying the inverse ring hom to the forward ring hom returns x: e.symm.toRingHom (e.toRingHom x) = x.

Русский

Пусть e — кольцевое эквивалентно между R и S. Для любого x ∈ R выполняется e.symm.toRingHom (e.toRingHom x) = x.

LaTeX

$$$ \forall x \in R,\ e.symm.toRingHom (e.toRingHom x) = x $$$

Lean4

theorem symm_toRingHom_apply_toRingHom_apply (e : R ≃+* S) : ∀ x : R, e.symm.toRingHom (e.toRingHom x) = x :=
  Equiv.symm_apply_apply e.toEquiv

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