Theorem Finsupp.degree_def

Modification history

2025-11-28 14:12
Mathlib/Data/Finsupp/Weight.lean
chore(Data/Finsupp): Rename degree_def (#32179)
Deleted Finsupp.degree_defView on Github →
2025-11-26 13:56
Mathlib/Data/Finsupp/Weight.lean
feat(Data/Finsupp): add degree_sum (#32074)
Added Finsupp.degree_defView on Github →