Commit 2024-01-16 15:36 e72937a7

View on Github →

refactor(MonoidAlgebra/Support): reformulate support_mul (#8953) Use pointwise multiplication/addition of Finsets in MonoidAlgebra.support_mul and AddMonoidAlgebra.support_mul.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/Algebra/MonoidAlgebra/Grading.lean

Modified Mathlib/Algebra/MonoidAlgebra/Support.lean

added theorem AddMonoidAlgebra.support_one

added theorem AddMonoidAlgebra.support_one_subset

added theorem MonoidAlgebra.support_one

added theorem MonoidAlgebra.support_one_subset

Modified Mathlib/Data/MvPolynomial/Basic.lean

Modified Mathlib/Data/MvPolynomial/Variables.lean

modified theorem MvPolynomial.degrees_pow

Modified Mathlib/Data/Polynomial/Coeff.lean