Theorems · Theorem · field theory

Polynomial.eq_X_sub_C_of_separable_of_root_eq

∀ {F : Type u} [inst : Field F] {K : Type v} [inst_1 : Field K] {i : F →+* K} {x : F} {h : Polynomial F},
  h.Separable →
    Polynomial.eval x h = 0 →
      (Polynomial.map i h).Splits →
        (∀ y ∈ (Polynomial.map i h).roots, y = i x) → h = Polynomial.C h.leadingCoeff * (Polynomial.X - Polynomial.C x)

Defined in

Mathlib.FieldTheory.Separable

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldField