basic): There is exactly one set in empty types (#15607)

Commit

3 years ago

feat(data/finset/basic): There is exactly one set in empty types (#15607) and transfer a few boolean algebra lemmas to `finset`.

Author

YaelDillies

Parents