Commit 2024-07-21 13:06 be1d8aff

feat (Data.Finsupp.Weight) : general API for weights and size of finsupp (#14875) We collect various definitions and lemma that are presently used for multivariate polynomials to define/study their degree / weighted degree in a single file Mathlib.Data.Finsupp.Weight`` The reason is that this API will also be used for multivariate power series. We have tried for some generality, but it is not the maximal one. Adds aSMulPosMono ℕ Minstance for anyOrderedAddCommMonoid M` Co-authored-by María Inés de Frutos Fernández @mariainesdff Moves:

• MvPolynomial.degree -> Finsupp.degree
• MvPolynomial.weightedDegree -> Finsupp.weight
• MvPolynomial.degree_eq_zero_iff -> Finsupp.degree_eq_zero_iff
• MvPolynomial.weightedDegree_one -> Finsupp.degree_eq_weight_one
• MvPolynomial.weight_eq_zero_iff_eq_zero_iff -> Finsupp.weight_eq_zero_iff_eq_zero