polyCost_pos

formal source

 197
 198/-- If `f` is a nonzero non-unit polynomial over a field with `q ≥ 2`,
 199    then `polyCost f > 0`. -/
 200theorem polyCost_pos {f : Polynomial F}
 201    (hf : f ≠ 0) (h_not_unit : ¬ IsUnit f)
 202    (hF : 2 ≤ Fintype.card F) :
 203    0 < polyCost f := by
 204  -- Since f is a nonzero non-unit, normalizedFactors f is nonempty.
 205  have h_factors_ne : normalizedFactors f ≠ 0 := by
 206    intro h_empty
 207    have h_prod : (normalizedFactors f).prod = normalize f :=
 208      prod_normalizedFactors_eq hf
 209    rw [h_empty, Multiset.prod_zero] at h_prod
 210    have h_norm_unit : IsUnit (normalize f) := h_prod ▸ isUnit_one
 211    have h_f_unit : IsUnit f :=
 212      (associated_normalize f).symm.isUnit h_norm_unit
 213    exact h_not_unit h_f_unit
 214  -- Pick a factor P from normalizedFactors f.
 215  obtain ⟨P, hP_mem⟩ := Multiset.exists_mem_of_ne_zero h_factors_ne
 216  have hP_irr : Irreducible P := irreducible_of_normalized_factor P hP_mem
 217  have hP_deg : 0 < P.natDegree := irreducible_natDegree_pos hP_irr
 218  have hP_pos : 0 < polyPrimeCost P := polyPrimeCost_pos hP_deg hF
 219  -- Decompose the multiset sum: P contributes hP_pos, others ≥ 0.
 220  unfold polyCost
 221  have h_decomp :
 222      (normalizedFactors f).map polyPrimeCost
 223        = polyPrimeCost P ::ₘ ((normalizedFactors f).erase P).map polyPrimeCost := by
 224    rw [← Multiset.map_cons polyPrimeCost P]
 225    congr 1
 226    exact (Multiset.cons_erase hP_mem).symm
 227  rw [h_decomp, Multiset.sum_cons]
 228  apply add_pos_of_pos_of_nonneg hP_pos
 229  apply Multiset.sum_nonneg
 230  intro x hx