Theorems · Theorem · field theory

IntermediateField.splits_of_mem_adjoin

∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] {L : Type u_3}
  [inst_3 : Field L] [inst_4 : Algebra F L] {S : Set K},
  (∀ x ∈ S, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
    ∀ {x : K}, x ∈ IntermediateField.adjoin F S → (Polynomial.map (algebraMap F L) (minpoly F x)).Splits

If a set of algebraic elements in a field extension K/F have minimal polynomials that split in another extension L/F, then all minimal polynomials in the intermediate field generated by the set also split in L/F.

Defined in

Mathlib.FieldTheory.Normal.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebra