Theorem Finsupp.nontrivial_iff

Modification history

2026-03-10 11:05
Mathlib/Data/Finsupp/Single.lean
feat(Data/Finsupp): characterise when `Finsupp` is `Nontrivial` (#35764) …
Added Finsupp.nontrivial_iffView on Github →