Theorems · Theorem · field theory

Algebra.IsAlgebraic.isNormalClosure_iff

∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [Algebra.IsAlgebraic F K],
  IsNormalClosure F K L ↔
    (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) ∧ IntermediateField.normalClosure F K L = ⊤

If K/F is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced by "generated by images of embeddings".

Defined in

Mathlib.FieldTheory.Normal.Closure

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraAlgebra.IsAlgebraic