Theorems · Theorem · field theory

isSplittingField_iff_intermediateField

∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {p : Polynomial K},
  Polynomial.IsSplittingField K L p ↔
    (Polynomial.map (algebraMap K L) p).Splits ∧ IntermediateField.adjoin K (p.rootSet L) = ⊤

Characterize IsSplittingField with IntermediateField.adjoin instead of Algebra.adjoin.

Defined in

Mathlib.FieldTheory.SplittingField.IsSplittingField

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra