From 54d1ddd2f1f08e4d0f1066bc681bc428afeba03a Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Mon, 25 Apr 2022 00:39:20 +0000
Subject: [PATCH] feat(algebra/polynomial/big_operators): add a lemma, reduce
 assumptions, golf (#13264)

---
 src/algebra/polynomial/big_operators.lean   | 32 +++++++++++++++------
 src/data/polynomial/degree/definitions.lean |  2 +-
 2 files changed, 24 insertions(+), 10 deletions(-)

diff --git a/src/algebra/polynomial/big_operators.lean b/src/algebra/polynomial/big_operators.lean
index a0a3f285921e0..9f48a03f1f5af 100644
--- a/src/algebra/polynomial/big_operators.lean
+++ b/src/algebra/polynomial/big_operators.lean
@@ -277,7 +277,23 @@ by simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using
 end comm_ring
 
 section no_zero_divisors
-variables [comm_ring R] [no_zero_divisors R] (f : ι → R[X]) (t : multiset R[X])
+
+section semiring
+variables [semiring R] [no_zero_divisors R]
+
+/--
+The degree of a product of polynomials is equal to
+the sum of the degrees, where the degree of the zero polynomial is ⊥.
+`[nontrivial R]` is needed, otherwise for `l = []` we have `⊥` in the LHS and `0` in the RHS.
+-/
+lemma degree_list_prod [nontrivial R] (l : list R[X]) :
+  l.prod.degree = (l.map degree).sum :=
+map_list_prod (@degree_monoid_hom R _ _ _) l
+
+end semiring
+
+section comm_semiring
+variables [comm_semiring R] [no_zero_divisors R] (f : ι → R[X]) (t : multiset R[X])
 
 /--
 The degree of a product of polynomials is equal to
@@ -295,9 +311,8 @@ begin
   intros x hx, simp [h x hx]
 end
 
-lemma nat_degree_multiset_prod (s : multiset R[X])
-  (h : (0 : R[X]) ∉ s) :
-  nat_degree s.prod = (s.map nat_degree).sum :=
+lemma nat_degree_multiset_prod (h : (0 : R[X]) ∉ t) :
+  nat_degree t.prod = (t.map nat_degree).sum :=
 begin
   nontriviality R,
   rw nat_degree_multiset_prod',
@@ -312,17 +327,14 @@ the sum of the degrees, where the degree of the zero polynomial is ⊥.
 -/
 lemma degree_multiset_prod [nontrivial R] :
   t.prod.degree = (t.map (λ f, degree f)).sum :=
-begin
-  refine multiset.induction_on t _ (λ a t ht, _), { simp },
-  { rw [multiset.prod_cons, degree_mul, ht, map_cons, multiset.sum_cons] }
-end
+map_multiset_prod (@degree_monoid_hom R _ _ _) _
 
 /--
 The degree of a product of polynomials is equal to
 the sum of the degrees, where the degree of the zero polynomial is ⊥.
 -/
 lemma degree_prod [nontrivial R] : (∏ i in s, f i).degree = ∑ i in s, (f i).degree :=
-by simpa using degree_multiset_prod (s.1.map f)
+map_prod (@degree_monoid_hom R _ _ _) _ _
 
 /--
 The leading coefficient of a product of polynomials is equal to
@@ -346,5 +358,7 @@ lemma leading_coeff_prod :
   (∏ i in s, f i).leading_coeff = ∏ i in s, (f i).leading_coeff :=
 by simpa using leading_coeff_multiset_prod (s.1.map f)
 
+end comm_semiring
+
 end no_zero_divisors
 end polynomial
diff --git a/src/data/polynomial/degree/definitions.lean b/src/data/polynomial/degree/definitions.lean
index 82eb9ffaf1c16..7fdca44f69ed9 100644
--- a/src/data/polynomial/degree/definitions.lean
+++ b/src/data/polynomial/degree/definitions.lean
@@ -1189,7 +1189,7 @@ def degree_monoid_hom [nontrivial R] : R[X] →* multiplicative (with_bot ℕ) :
 
 @[simp] lemma degree_pow [nontrivial R] (p : R[X]) (n : ℕ) :
   degree (p ^ n) = n • (degree p) :=
-map_pow (degree_monoid_hom : R[X] →* _) _ _
+map_pow (@degree_monoid_hom R _ _ _) _ _
 
 @[simp] lemma leading_coeff_mul (p q : R[X]) : leading_coeff (p * q) =
   leading_coeff p * leading_coeff q :=