English
If L is an intermediate field over F in a tower F ⊆ E ⊆ K and E/F is algebraic, then rank_E(adjoin_E(L)) ≤ rank_F L.
Русский
Если E/F алгебраично, тогда rank_E(adjoin_E(L)) ≤ rank_F L.
LaTeX
$$$\operatorname{rank}_E(\mathrm{adjoin}_E(L)) \le \operatorname{rank}_F(L)$$$
Lean4
/-- If `K / E / F` is a field extension tower, `L` is an intermediate field of `K / F`, such that
either `E / F` or `L / F` is algebraic, then `[E(L) : E] ≤ [L : F]`. A corollary of
`Subalgebra.adjoin_rank_le` since in this case `E(L) = E[L]`. -/
theorem adjoin_rank_le_of_isAlgebraic (L : IntermediateField F K)
(halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F L) :
Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L :=
by
have h : (adjoin E (L.toSubalgebra : Set K)).toSubalgebra = Algebra.adjoin E (L.toSubalgebra : Set K) :=
L.adjoin_toSubalgebra_of_isAlgebraic E halg
have := L.toSubalgebra.adjoin_rank_le E
rwa [(Subalgebra.equivOfEq _ _ h).symm.toLinearEquiv.rank_eq] at this
