Theorem Finsupp.nonTorsionWeight_of

Modification history

2026-01-13 19:40

Mathlib/Data/Finsupp/Weight.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Modified Finsupp.nonTorsionWeight_of View on Github →

2025-01-30 22:16

Mathlib/Data/Finsupp/Weight.lean

refactor(Data/Finsupp/Weight): generalize and add lemmas (#20635) …

Modified Finsupp.nonTorsionWeight_of View on Github →

2024-07-21 13:06

Mathlib/Data/Finsupp/Weight.lean

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

Added Finsupp.nonTorsionWeight_of View on Github →