Theorems · Definition · field theory

Polynomial.SplittingField.lift

{K : Type v} →
  {L : Type w} →
    [inst : Field K] →
      [inst_1 : Field L] →
        (f : Polynomial K) →
          [inst_2 : Algebra K L] → (Polynomial.map (algebraMap K L) f).Splits → f.SplittingField →ₐ[K] L

Embeds the splitting field into any other field that splits the polynomial.

Defined in: Mathlib.FieldTheory.SplittingField.Construction
Cited by: 2 results in Mathlib
Foundations: Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Algebrastatement and proof · cited by 11,388
Fieldstatement and proof · cited by 7,404
Polynomialstatement and proof · cited by 5,681
Algebra.algebraMapstatement and proof · cited by 4,706
AlgHomstatement · cited by 3,236
Polynomial.mapstatement and proof · cited by 806
Polynomial.Splitsstatement and proof · cited by 290
Polynomial.SplittingFieldstatement and proof · cited by 42
Polynomial.IsSplittingField.liftproof · cited by 2

Cited by2

Results whose statement or proof uses this declaration.

Polynomial.natSepDegree_eq_of_splitsproof · cited by 2
Polynomial.Gal.mul_splits_in_splittingField_of_mulproof · cited by 1