polyCost_le_mul

formal source

 165    ring
 166
 167/-- Cost is monotonic under multiplication by nonzero polynomials. -/
 168theorem polyCost_le_mul {f g : Polynomial F} (hf : f ≠ 0) (hg : g ≠ 0) :
 169    polyCost f ≤ polyCost (f * g) := by
 170  rw [polyCost_mul hf hg]
 171  have := polyCost_nonneg g
 172  linarith
 173
 174/-! ## Strict positivity for non-units -/
 175
 176/-- An irreducible polynomial over a field has positive `natDegree`.
 177    A polynomial with `natDegree = 0` is either zero or a unit;
 178    irreducibles are neither. -/
 179private lemma irreducible_natDegree_pos {P : Polynomial F}
 180    (hP_irr : Irreducible P) : 0 < P.natDegree := by
 181  rw [Nat.pos_iff_ne_zero]
 182  intro h_zero
 183  have hP_ne : P ≠ 0 := hP_irr.ne_zero
 184  -- natDegree = 0 ⟹ P = C (coeff P 0).
 185  obtain ⟨c, hc⟩ := Polynomial.natDegree_eq_zero.mp h_zero
 186  -- coeff P 0 ≠ 0 because P ≠ 0.
 187  have hc_ne : c ≠ 0 := by
 188    intro h_c_zero
 189    apply hP_ne
 190    rw [← hc, h_c_zero]
 191    simp
 192  -- A constant polynomial with nonzero constant is a unit in F[X].
 193  have hP_unit : IsUnit P := by
 194    rw [← hc]
 195    exact Polynomial.isUnit_C.mpr (isUnit_iff_ne_zero.mpr hc_ne)
 196  exact hP_irr.not_isUnit hP_unit
 197
 198/-- If `f` is a nonzero non-unit polynomial over a field with `q ≥ 2`,