English
Let t be a multiset of polynomials in R[X], and assume every element is monic. Then degree(t.prod) = ∑ degree(p) over p ∈ t.
Русский
Пусть t — мультисет многочленов, каждый из которых моничен. Тогда degree(т.произведение) равно сумме степеней каждого члена.
LaTeX
$$$$\left(\forall f \in t, \operatorname{Monic}(f)\right) \implies \operatorname{degree}\left( t.prod \right) = \sum_{f \in t} \operatorname{degree}(f).$$$$
Lean4
theorem degree_multiset_prod_of_monic [Nontrivial R] (h : ∀ f ∈ t, Monic f) : t.prod.degree = (t.map degree).sum :=
by
have : t.prod ≠ 0 := Monic.ne_zero <| by simpa using monic_multiset_prod_of_monic _ _ h
rw [degree_eq_natDegree this, natDegree_multiset_prod_of_monic _ h, Nat.cast_multiset_sum, Multiset.map_map,
Function.comp_def, Multiset.map_congr rfl (fun f hf => (degree_eq_natDegree (h f hf).ne_zero).symm)]
