mathlib3
08648056 - feat(data/finset/basic): Add `decidable_nonempty` for finsets. (#15170)

Commit
3 years ago
feat(data/finset/basic): Add `decidable_nonempty` for finsets. (#15170) Also remove some redundant decidable instances in multiset and list. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>
Parents
Loading