big_operators): lemmas about polynomial degree of products (#11258)

Commit

4 years ago

feat(algebra/polynomial/big_operators): lemmas about polynomial degree of products (#11258) These already existed for `nat_degree` but `degree` versions seemed missing. from flt-regular

Author

alexjbest

Parents

a1f4ac35

mathlib3 3ab1c1cb - feat(algebra/polynomial/big_operators): lemmas about polynomial degree of products (#11258)

mathlib3
3ab1c1cb - feat(algebra/polynomial/big_operators): lemmas about polynomial degree of products (#11258)