Theorems · Theorem · field theory

IntermediateField.splits_iff_mem

∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {p : Polynomial K}
  {F : IntermediateField K L},
  (Polynomial.map (algebraMap K L) p).Splits → ((Polynomial.map (algebraMap K ↥F) p).Splits ↔ ∀ x ∈ p.rootSet L, x ∈ F)

Defined in

Mathlib.FieldTheory.SplittingField.IsSplittingField

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra