Commit 2021-08-27 15:28 c4cf4c25

View on Github →

feat(algebra/polynomial/big_operators): coeff of sums and prods of polynomials (#8680) Additionally, provide results for degree and nat_degree over lists, which generalize away from requiring commutativity.

Estimated changes

Modified src/algebra/polynomial/big_operators.lean

added theorem polynomial.coeff_list_prod_of_nat_degree_le

added theorem polynomial.coeff_multiset_prod_of_nat_degree_le

added theorem polynomial.coeff_prod_of_nat_degree_le

added theorem polynomial.degree_list_sum_le

modified theorem polynomial.leading_coeff_multiset_prod'

added theorem polynomial.nat_degree_list_prod_le

added theorem polynomial.nat_degree_list_sum_le

added theorem polynomial.nat_degree_multiset_sum_le

added theorem polynomial.nat_degree_sum_le

Modified src/data/list/basic.lean

added theorem list.sum_le_foldr_max