adjoin_le_subfield — Mathlib

English

If the range of algebraMap F E and S are contained in a subfield K of E, then adjoin F S (as a subfield) is contained in K.

Русский

Пусть диапазон algebraMap F E и множество S содержатся в подполе K; тогда adjoin F S ⊆ K.

LaTeX

$$$\text{HF}:= \operatorname{range}(\mathrm{algebraMap}_{F,E}) \subseteq K \text{ and } HS: S \subseteq K \Rightarrow (\operatorname{adjoin}_F S)^{\text{toSubfield}} \le K$$$

Lean4

/-- If `K` is a field with `F ⊆ K` and `S ⊆ K` then `adjoin F S ≤ K`. -/
theorem adjoin_le_subfield {K : Subfield E} (HF : Set.range (algebraMap F E) ⊆ K) (HS : S ⊆ K) :
    (adjoin F S).toSubfield ≤ K := by
  apply Subfield.closure_le.mpr
  rw [Set.union_subset_iff]
  exact ⟨HF, HS⟩

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