Theorems · Theorem · field theory

IntermediateField.adjoin_intermediateField_toSubalgebra_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 →
    (IntermediateField.adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑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].

Defined in

Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebraAlgebraIsScalarTower