Theorems · Theorem · field theory

IntermediateField.Lifts.exists_lift_of_splits

∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] (x : IntermediateField.Lifts F E K) {s : E},
  IsIntegral F s → (Polynomial.map (algebraMap F K) (minpoly F s)).Splits → ∃ y, x ≤ y ∧ s ∈ y.carrier

Given an integral element s : E over F whose F-conjugates are all in K, any lift can be extended to one whose carrier contains s.

Defined in

Mathlib.FieldTheory.Extension

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebra