English
Same as above, in the alternative formulation natDegree t.prod = (t.map natDegree).sum when t contains no zero.
Русский
То же самое в альтернативной формулировке: natDegree t.prod = (t.map natDegree).sum при отсутствии нулевого элемента в t.
LaTeX
$$$$\operatorname{natDegree}(t.prod) = \sum_{p\in t} \operatorname{natDegree}(p) \,\text{whenever } 0 \notin t.$$$$
Lean4
/-- The degree of a product of polynomials is equal to
the sum of the degrees.
See `Polynomial.natDegree_prod'` (with a `'`) for a version for commutative semirings,
where additionally, the product of the leading coefficients must be nonzero.
-/
theorem natDegree_prod (h : ∀ i ∈ s, f i ≠ 0) : (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree :=
by
nontriviality R
apply natDegree_prod'
rw [prod_ne_zero_iff]
intro x hx; simp [h x hx]
