mathlib

d32bb6ed - feat(data/finsupp/basic): add support_nonempty_iff and nonzero_iff_exists (#6530)

feat(data/finsupp/basic): add support_nonempty_iff and nonzero_iff_exists (#6530) Add two lemmas to work with `finsupp`s with non-empty support. Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/finsupp.2Enonzero_iff_exists