Commit 2025-11-26 13:56 b25a4f77

View on Github →

feat(Data/Finsupp): add degree_sum (#32074)

Estimated changes

Modified Mathlib/Combinatorics/Nullstellensatz.lean

Modified Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

Modified Mathlib/Data/Finsupp/Weight.lean

modified def Finsupp.degree

deleted theorem Finsupp.degree_add

added theorem Finsupp.degree_def

deleted theorem Finsupp.degree_zero

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean