Theorems · Theorem · field theory

IntermediateField.adjoin_rank_le_of_isAlgebraic

∀ {F : Type u_1} [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K),
  Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L → Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L

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].

Defined in

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Cited by

2 results in Mathlib

Foundations

Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraFieldAlgebraAlgebraIsScalarTower