Theorem Finsupp.le_weight_of_ne_zero'

Modification history

2026-04-29 14:11

Mathlib/Data/Finsupp/Weight.lean

chore: make argument in `zero_le`/`one_le` implicit (#38148) …

Modified Finsupp.le_weight_of_ne_zero'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.le_weight_of_ne_zero'View on Github →