 154  simp
 155
 156/-- Cost on a power: `c(P^k) = k · c(P)` for any nonzero `P`. -/
 157theorem polyCost_pow {P : Polynomial F} (hP : P ≠ 0) (k : ℕ) :
 158    polyCost (P ^ k) = (k : ℝ) * polyCost P := by
 159  induction k with
 160  | zero => simp [polyCost_one]
 161  | succ k ih =>
 162    have hPk : P ^ k ≠ 0 := pow_ne_zero k hP
 163    rw [pow_succ, polyCost_mul hPk hP, ih]
 164    push_cast
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.