Binomial irreducibility and finite-field noncubes

Mathlib's odd-prime-power binomial irreducibility theorem gives the modulus family. Cauchy's theorem gives a nontrivial cube root of unity when three divides the unit-group order. Cubing is then noninjective and hence nonsurjective on the finite field.

theorem Algebraic.Cutwidth.Extractor.Internal.binomialModulus_monic {F : Type u_1} [Ring F] (a : F) (s : ℕ) : (binomialModulus a s).Monic

theorem Algebraic.Cutwidth.Extractor.Internal.binomialModulus_natDegree {F : Type u_1} [Ring F] [Nontrivial F] (a : F) (s : ℕ) : (binomialModulus a s).natDegree = 3 ^ s

theorem Algebraic.Cutwidth.Extractor.Internal.binomialModulus_irreducible {F : Type u_1} [Field F] (a : F) (s : ℕ) (noncube : ∀ (b : F), b ^ 3 ≠ a) : Irreducible (binomialModulus a s)

theorem Algebraic.Cutwidth.Extractor.Internal.exists_noncube {F : Type u_1} [Field F] [Fintype F] (divisible : 3 ∣ Fintype.card F - 1) : ∃ (a : F), ∀ (b : F), b ^ 3 ≠ a

theorem Algebraic.Cutwidth.Extractor.Internal.three_dvd_card_sub_one_of_even_exponent {F : Type u_1} [Fintype F] {b : ℕ} (cardinality : Fintype.card F = 2 ^ b) (even : Even b) : 3 ∣ Fintype.card F - 1

theorem Algebraic.Cutwidth.Extractor.Internal.binomialModulus_natDegree_clog_bounds {F : Type u_1} [Ring F] [Nontrivial F] (a : F) {n : ℕ} (positive : 0 < n) : n ≤ (binomialModulus a (Nat.clog 3 n)).natDegree ∧ (binomialModulus a (Nat.clog 3 n)).natDegree < 3 * n