Commit 2026-03-10 11:05 28e28bb8

View on Github →

feat(Data/Finsupp): characterise when Finsupp is Nontrivial (#35764) From ClassFieldTheory

Estimated changes

Modified Mathlib/Data/Finsupp/Defs.lean

modified theorem Finsupp.nontrivial_of_nontrivial

Modified Mathlib/Data/Finsupp/Single.lean

added theorem Finsupp.nontrivial_iff