Commit 2023-05-06 19:50 abcee9df

View on Github →

feat(Data/MvPolynomial/Basic): add and generalize some lemmas from Finsupp and MonoidAlgebra (#3604) Most of these changes generalize from DistribMulAction to SmulZeroClass. The new lemmas are all just proved using corresponding lemmas on the underlying types.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

Modified Mathlib/Data/Finsupp/Basic.lean

modified theorem Finsupp.support_smul

Modified Mathlib/Data/MvPolynomial/Basic.lean

modified theorem MvPolynomial.aevalTower_id

modified theorem MvPolynomial.coeff_smul

modified theorem MvPolynomial.constantCoeff_smul

added theorem MvPolynomial.smul_monomial

added theorem MvPolynomial.support_eq_empty

modified theorem MvPolynomial.support_smul

added theorem MvPolynomial.support_smul_eq