Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-11-25 18:11
36463426
View on Github →
feat(MvPolynomial): more lemmas about
finSuccEquiv
(
#19201
)
Estimated changes
Modified
Mathlib/Algebra/MvPolynomial/Equiv.lean
modified
theorem
MvPolynomial.finSuccEquiv_X_zero
deleted
theorem
MvPolynomial.finSuccEquiv_support'
deleted
theorem
MvPolynomial.finSuccEquiv_support
added
theorem
MvPolynomial.image_support_finSuccEquiv
added
theorem
MvPolynomial.mem_image_support_coeff_finSuccEquiv
added
theorem
MvPolynomial.mem_support_coeff_finSuccEquiv
added
theorem
MvPolynomial.mem_support_finSuccEquiv
added
theorem
MvPolynomial.support_finSuccEquiv
Modified
Mathlib/Data/Finsupp/Fin.lean
added
theorem
Finsupp.cons_right_injective