Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 19:47 fb82d0a5

View on Github →

feat(data/mv_polynomial/basic): add a symmetric version of coeff_X_mul and generalize to monomials (#10429)

Estimated changes

Modified src/algebra/monoid_algebra/basic.lean

added theorem add_monoid_algebra.support_single_mul

added theorem monoid_algebra.support_single_mul

Modified src/data/mv_polynomial/basic.lean

added theorem mv_polynomial.coeff_X_mul'

added theorem mv_polynomial.coeff_X_mul

added theorem mv_polynomial.coeff_monomial_mul'

added theorem mv_polynomial.coeff_monomial_mul

added theorem mv_polynomial.coeff_mul_monomial'

added theorem mv_polynomial.coeff_mul_monomial

modified theorem mv_polynomial.map_alg_hom_coe_ring_hom

added theorem mv_polynomial.support_X_mul