English
Let s be a finite index set and f_i ∈ R[X]. If the product of leading coefficients ∏_{i∈s} leadingCoeff(f_i) is nonzero, then natDegree(∏_{i∈s} f_i) = ∑_{i∈s} natDegree(f_i).
Русский
Пусть s — конечное множество индексов и f_i ∈ R[X]. Если произведение ведущих коэффициентов ∏_{i∈s} leadingCoeff(f_i) не равно нулю, то natDegree(∏_{i∈s} f_i) = ∑_{i∈s} natDegree(f_i).
LaTeX
$$$$\left(\prod_{i\in s} (f_i).leadingCoeff\right) \neq 0 \implies \left(\prod_{i\in s} f_i\right).natDegree = \sum_{i\in s} (f_i).natDegree.$$$$
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_prod` (without the `'`) for a version for integral domains,
where this condition is automatically satisfied.
-/
theorem natDegree_prod' (h : (∏ i ∈ s, (f i).leadingCoeff) ≠ 0) : (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree :=
by simpa using natDegree_multiset_prod' (s.1.map f) (by simpa using h)
