Theorems · Theorem · field theory

Polynomial.lift_of_splits

∀ {F : Type u_2} {K : Type u_3} {L : Type u_4} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] (s : Finset K),
  (∀ x ∈ s, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
    Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)

If K and L are field extensions of F and we have s : Finset K such that the minimal polynomial of each x ∈ s splits in L then Algebra.adjoin F s embeds in L.

Defined in

Mathlib.RingTheory.Adjoin.Field

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebra