pith. machine review for the scientific record. sign in
theorem proved term proof

polyCost_le_mul

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 168theorem polyCost_le_mul {f g : Polynomial F} (hf : f ≠ 0) (hg : g ≠ 0) :
 169    polyCost f ≤ polyCost (f * g) := by

proof body

Term-mode proof.

 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. -/

depends on (16)

Lean names referenced from this declaration's body.