Merge remote-tracking branch 'origin/master' into bump/v4.14.0

Mathlib/Algebra/Polynomial/BigOperators.lean

@@ -193,10 +193,21 @@ theorem natDegree_multiset_prod_of_monic (h : ∀ f ∈ t, Monic f) :
     assumption
   · simp
 
+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)]
+
 theorem natDegree_prod_of_monic (h : ∀ i ∈ s, (f i).Monic) :
     (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree := by
   simpa using natDegree_multiset_prod_of_monic (s.1.map f) (by simpa using h)
 
+theorem degree_prod_of_monic [Nontrivial R] (h : ∀ i ∈ s, (f i).Monic) :
+    (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree := by
+  simpa using degree_multiset_prod_of_monic (s.1.map f) (by simpa using h)
+
 theorem coeff_multiset_prod_of_natDegree_le (n : ℕ) (hl : ∀ p ∈ t, natDegree p ≤ n) :
     coeff t.prod ((Multiset.card t) * n) = (t.map fun p => coeff p n).prod := by
   induction t using Quotient.inductionOn