Commit 2021-05-01 06:41 2cc8128f

View on Github →

feat(algebra/polynomial): generalize to multiset products (#7399) This PR generalizes the results in algebra.polynomial.big_operators to sums and products of multisets. The new multiset results are stated for multiset.prod t, not (multiset.map t f).prod. To get the latter, you can simply rewrite with multiset.map_map.

Estimated changes

Modified src/algebra/polynomial/big_operators.lean

added theorem polynomial.coeff_zero_multiset_prod

added theorem polynomial.degree_multiset_prod

added theorem polynomial.leading_coeff_multiset_prod'

added theorem polynomial.leading_coeff_multiset_prod

added theorem polynomial.multiset_prod_X_sub_C_coeff_card_pred

added theorem polynomial.multiset_prod_X_sub_C_next_coeff

added theorem polynomial.nat_degree_multiset_prod'

added theorem polynomial.nat_degree_multiset_prod_le

added theorem polynomial.nat_degree_multiset_prod_of_monic

Modified src/data/polynomial/monic.lean

added theorem polynomial.monic.next_coeff_multiset_prod

added theorem polynomial.monic_multiset_prod_of_monic