Theorems · Theorem · field theory

minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow

∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Ring E] [IsDomain E] [inst_3 : Algebra F E] (q : ℕ)
  [hF : ExpChar F q] {x : E},
  (minpoly F x).natSepDegree = 1 ↔
    ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n

The minimal polynomial of an element x of E / F of exponential characteristic q has separable degree one if and only if the minimal polynomial is of the form (X - x) ^ (q ^ n) for some n : ℕ.

Defined in

Mathlib.FieldTheory.SeparableDegree

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldRingIsDomainAlgebraExpChar