Commit 2025-10-27 15:02 65a039af

View on Github →

feat(MvPolynomial/Expand): more lemmas (#28833)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

modified theorem MvPolynomial.aeval_X

added theorem MvPolynomial.aeval_eq_eval

modified theorem MvPolynomial.coe_aeval_eq_eval

Modified Mathlib/Algebra/MvPolynomial/Expand.lean

added theorem MvPolynomial.aeval_comp_expand

added theorem MvPolynomial.aeval_expand

added theorem MvPolynomial.coeff_expand_of_not_dvd

added theorem MvPolynomial.coeff_expand_smul

added theorem MvPolynomial.eval_expand

added theorem MvPolynomial.eval₂Hom_comp_expand

added theorem MvPolynomial.eval₂_expand

added theorem MvPolynomial.expand_mul

added theorem MvPolynomial.expand_mul_eq_comp

modified theorem MvPolynomial.expand_one_apply

added theorem MvPolynomial.expand_zero

added theorem MvPolynomial.expand_zero_apply

added theorem MvPolynomial.support_expand

added theorem MvPolynomial.support_expand_subset