Commit 2025-11-28 14:12 4bb77eb8

View on Github →

chore(Data/Finsupp): Rename degree_def (#32179)

Estimated changes

Modified Mathlib/Combinatorics/Nullstellensatz.lean

Modified Mathlib/Data/Finsupp/Weight.lean

added theorem Finsupp.degree_apply

deleted theorem Finsupp.degree_def

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean