Commit 2023-03-09 14:54 fef1c8fe

View on Github →

feat: port Algebra.Polynomial.BigOperators (#2750)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Polynomial/BigOperators.lean

added theorem Polynomial.coeff_list_prod_of_natDegree_le

added theorem Polynomial.coeff_multiset_prod_of_natDegree_le

added theorem Polynomial.coeff_prod_of_natDegree_le

added theorem Polynomial.coeff_zero_multiset_prod

added theorem Polynomial.coeff_zero_prod

added theorem Polynomial.degree_list_prod

added theorem Polynomial.degree_list_prod_le

added theorem Polynomial.degree_list_sum_le

added theorem Polynomial.degree_multiset_prod

added theorem Polynomial.degree_multiset_prod_le

added theorem Polynomial.degree_prod

added theorem Polynomial.degree_prod_le

added theorem Polynomial.leadingCoeff_multiset_prod'

added theorem Polynomial.leadingCoeff_multiset_prod

added theorem Polynomial.leadingCoeff_prod'

added theorem Polynomial.leadingCoeff_prod

added theorem Polynomial.multiset_prod_X_sub_C_coeff_card_pred

added theorem Polynomial.multiset_prod_X_sub_C_nextCoeff

added theorem Polynomial.natDegree_list_prod_le

added theorem Polynomial.natDegree_list_sum_le

added theorem Polynomial.natDegree_multiset_prod'

added theorem Polynomial.natDegree_multiset_prod

added theorem Polynomial.natDegree_multiset_prod_le

added theorem Polynomial.natDegree_multiset_prod_of_monic

added theorem Polynomial.natDegree_multiset_sum_le

added theorem Polynomial.natDegree_prod'

added theorem Polynomial.natDegree_prod

added theorem Polynomial.natDegree_prod_le

added theorem Polynomial.natDegree_prod_of_monic

added theorem Polynomial.natDegree_sum_le

added theorem Polynomial.prod_X_sub_C_coeff_card_pred

added theorem Polynomial.prod_x_sub_c_nextCoeff