Commit 2026-03-27 13:44 f92dcbb6

View on Github →

feat(Algebra/MvPolynomial/Coeff): add lemmas (#36444) Co-authored by: @AntoineChambert-Loir.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.coeff_prod_X_pow

added theorem MvPolynomial.prod_X_pow

Created Mathlib/Algebra/MvPolynomial/Coeff.lean

added theorem MvPolynomial.coeff_add_pow

added theorem MvPolynomial.coeff_linearCombination_X_pow

added theorem MvPolynomial.coeff_linearCombination_X_pow_of_fintype

added theorem MvPolynomial.coeff_sum_X_pow_of_fintype

Modified Mathlib/Data/Fintype/Basic.lean

added theorem Finset.univ_fin2

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

added theorem Finsupp.multinomial_of_support_subset

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

deleted theorem Finset.univ_fin2