map_equiv_eq_comap_symm — Mathlib

English

For a RingEquiv f: R ≃+* S and a Subsemiring K of R, the image under f equals the comap under f.symm: K.map f = K.comap f.symm.

Русский

Для изоморфизма колец f: R ≃+* S и подпол semiring K ⊆ R, образ K под действием f равен обратному образу K.symm: K.map f = K.comap f.symm.

LaTeX

$$$K.map (f : R \\to+* S) = K.comap f.symm$$$

Lean4

theorem map_equiv_eq_comap_symm (f : R ≃+* S) (K : Subsemiring R) : K.map (f : R →+* S) = K.comap f.symm :=
  SetLike.coe_injective (f.toEquiv.image_eq_preimage K)

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