English
If the product of leading coefficients is nonzero, the natDegree of the product equals the sum of natDegrees.
Русский
Если произведение ведущих коэффициентов не нулевое, то натDegree произведения равна сумме natDegree факторов.
LaTeX
$$natDegree (t.prod) = (t.map natDegree).sum$$
Lean4
/-- The degree of a product of polynomials is equal to
the sum of the degrees, provided that the product of leading coefficients is nonzero.
See `Polynomial.natDegree_multiset_prod` (without the `'`) for a version for integral domains,
where this condition is automatically satisfied.
-/
theorem natDegree_multiset_prod' (h : (t.map fun f => leadingCoeff f).prod ≠ 0) :
t.prod.natDegree = (t.map fun f => natDegree f).sum :=
by
revert h
refine Multiset.induction_on t ?_ fun a t ih ht => ?_; · simp
rw [Multiset.map_cons, Multiset.prod_cons] at ht ⊢
rw [Multiset.sum_cons, Polynomial.natDegree_mul', ih]
· apply right_ne_zero_of_mul ht
· rwa [Polynomial.leadingCoeff_multiset_prod']
apply right_ne_zero_of_mul ht
