diff --git a/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean b/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean
index 397a3b99b..89aa986c3 100644
--- a/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean
+++ b/Complexity/Computability/Complexity/AffineDisperser/BinaryPolynomial.lean
@@ -320,10 +320,6 @@ theorem modBits_all_false_iff (l f : List Bool) :
     ← length_modBits l f]
   exact degree_polyOfBits_lt _
 
-/-- Every nonzero binary polynomial is monic. -/
-theorem monic_of_ne_zero {q : (ZMod 2)[X]} (hq : q ≠ 0) : q.Monic :=
-  (by decide : ∀ c : ZMod 2, c ≠ 0 → c = 1) _ (leadingCoeff_ne_zero.2 hq)
-
 private theorem natDegree_polyOfCode_eq_log (m : ℕ) : (polyOfCode m).natDegree = Nat.log 2 m := by
   rcases eq_or_ne m 0 with rfl | hm
   · simp
diff --git a/Complexity/Foundations/FieldTheory/Finite/BinaryField.lean b/Complexity/Foundations/FieldTheory/Finite/BinaryField.lean
index 5f96451e4..e67caf2a3 100644
--- a/Complexity/Foundations/FieldTheory/Finite/BinaryField.lean
+++ b/Complexity/Foundations/FieldTheory/Finite/BinaryField.lean
@@ -54,6 +54,7 @@ need `w ≠ 0`.
 
 ## Main results
 
+* `Cslib.monic_of_ne_zero`: every nonzero binary polynomial is monic.
 * `Cslib.irreducible_leastIrreducible`, `Cslib.monic_leastIrreducible`,
   `Cslib.natDegree_leastIrreducible`: `leastIrreducible w` is monic and irreducible, of degree `w`
   when `w ≠ 0`.
@@ -211,10 +212,13 @@ theorem exists_code_leastIrreducible {p : ℕ} (hp : p ≠ 0) :
   · exact hlog ▸ Nat.pow_log_le_self 2 hm0
   · exact hlog ▸ Nat.lt_pow_succ_log_self one_lt_two m
 
+/-- Every nonzero binary polynomial is monic. -/
+theorem monic_of_ne_zero {q : (ZMod 2)[X]} (hq : q ≠ 0) : q.Monic :=
+  (by decide : ∀ c : ZMod 2, c ≠ 0 → c = 1) _ (leadingCoeff_ne_zero.2 hq)
+
 /-- `leastIrreducible w` is monic for every degree `w`, as every nonzero binary polynomial is. -/
 theorem monic_leastIrreducible (w : ℕ) : (leastIrreducible w).Monic :=
-  (by decide : ∀ c : ZMod 2, c ≠ 0 → c = 1) _
-    (leadingCoeff_ne_zero.2 (irreducible_leastIrreducible w).ne_zero)
+  monic_of_ne_zero (irreducible_leastIrreducible w).ne_zero
 
 /-- **The explicit binary field of degree `w`**: binary polynomials modulo the irreducible
 polynomial of degree `w` with the least code. -/