map_inf — Mathlib

English

Let f be a ring homomorphism and s, t subfields of K. The image of the meet equals the meet of the images: (s ⊓ t).map f = s.map f ⊓ t.map f.

Русский

Пусть f — кольцеобразный гомоморфизм, и s, t — подполе K. Образ их пересечения равен пересечению образов: (s ⊓ t).map f = s.map f ⊓ t.map f.

LaTeX

$$$$(s \sqcap t).map f = s.map f \sqcap t.map f$$$$

Lean4

theorem map_inf (s t : Subfield K) (f : K →+* L) : (s ⊓ t).map f = s.map f ⊓ t.map f :=
  SetLike.coe_injective (Set.image_inter f.injective)

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