Theorems · Theorem · field theory

Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible

∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [inst_1 : ExpChar F q],
  f.Monic →
    Irreducible f →
      f.natSepDegree = 1 → ∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = Polynomial.X ^ q ^ n - Polynomial.C y

If a monic irreducible polynomial over a field F of exponential characteristic q has separable degree one, then it is of the form X ^ (q ^ n) - C y for some natural number n, and some element y of F, such that either n = 0 or y has no q-th root in F.

Defined in

Mathlib.FieldTheory.SeparableDegree

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldExpChar