map_equiv_eq_comap_symm — Mathlib

English

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

Русский

Для кольцевого эквивалента f: R ≃+* S и K ⊆ R: K.map f = K.comap f.symm.

LaTeX

$$$K.map f = K.comap f^{-1}$$$

Lean4

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

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