Theorem MvPolynomial.nonTorsionWeight_of

Modification history

2025-11-05 11:15

Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

chore: use `IsAddTorsionFree M` instead of `NoZeroSMulDivisors ℕ M`/`NoZeroSMulDivisors ℤ M` (#30683) …

Modified MvPolynomial.nonTorsionWeight_of View on Github →

2024-04-15 15:25

Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

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

Added MvPolynomial.nonTorsionWeight_of View on Github →