adjoin_eq_top_of_adjoin_eq_top — Mathlib

English

Let K ⊂ E ⊂ K̄ be a tower of fields with E over F and K over E, and S ⊆ K with F(S) = K. Then E(S) = K.

Русский

Пусть K ⊂ E ⊂ K векторное множество полей в башне F ⊆ E ⊆ K, где E является расширением F, K — над E, и S ⊆ K такое, что F(S) = K. Тогда E(S) = K.

LaTeX

$$$\operatorname{adjoin}_F(S) = \top \quad\Rightarrow\quad \operatorname{adjoin}_E(S) = \top$$$

Lean4

/-- If `K / E / F` is a field extension tower, `S ⊂ K` is such that `F(S) = K`,
then `E(S) = K`. -/
theorem adjoin_eq_top_of_adjoin_eq_top [Algebra E K] [IsScalarTower F E K] {S : Set K} (hprim : adjoin F S = ⊤) :
    adjoin E S = ⊤ :=
  restrictScalars_injective F <| by
    rw [restrictScalars_top, ← top_le_iff, ← hprim, adjoin_le_iff, coe_restrictScalars, ← adjoin_le_iff]

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