Commit 2021-03-04 11:33 d32bb6ed
View on Github →feat(data/finsupp/basic): add support_nonempty_iff and nonzero_iff_exists (#6530)
Add two lemmas to work with finsupps with non-empty support.
Zulip:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/finsupp.2Enonzero_iff_exists