∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q],
  f.Monic →
    Irreducible f → (f.natSepDegree = 1 ↔ ∃ n y, f = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y))