mathlib3

fa8df59b - feat(algebra/polynomial/big_operators): add degree_prod lemma (#5979)

feat(algebra/polynomial/big_operators): add degree_prod lemma (#5979) This PR adds a degree_prod lemma next to the nat_degree_prod lemma. This version of the lemma works for the interpretation of 'degree' which says the degree of the zero polynomial is \bot