Commit 2025-01-30 22:16 fbd1225c

View on Github →

refactor(Data/Finsupp/Weight): generalize and add lemmas (#20635) This consists on easy generalizations and lemmas relative to the weight of finsupp functions, that will be used in the formalization of Alon's combinatorial Nullstellensatz #20495

Estimated changes

modified def Finsupp.degree
modified theorem Finsupp.degree_add
modified theorem Finsupp.degree_eq_zero_iff
modified theorem Finsupp.degree_single
modified theorem Finsupp.degree_zero
modified theorem Finsupp.le_degree
modified theorem Finsupp.nonTorsionWeight_of
modified theorem Finsupp.weight_apply
added theorem Finsupp.weight_single