Def MvPolynomial.weightedDegree'

Modification history

2024-04-15 15:25

Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

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

Deleted MvPolynomial.weightedDegree'View on Github →

2023-03-31 10:48

Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

feat: port RingTheory.MvPolynomial.WeightedHomogeneous (#3192)

Added MvPolynomial.weightedDegree'View on Github →