Def MvPolynomial.degree

Modification history

2024-07-21 13:06

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

feat (Data.Finsupp.Weight) : general API for weights and size of finsupp (#14875) …

Deleted MvPolynomial.degree View on Github →

2024-05-27 08:32

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

chore: Use the new `∑ i ∈ s, f i` notation (#13209) …

Modified MvPolynomial.degree View on Github →

2024-04-15 15:25

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

refactor(RingTheory.MvPolynomial.Homogeneous): refactor in terms of weightedHomogeneous (#7609) …

Added MvPolynomial.degree View on Github →