mathlib
0c503262 - refactor(*): use `is_empty` instead of `not (nonempty α)` (#8858)

Commit

4 years ago

refactor(*): use `is_empty` instead of `not (nonempty α)` (#8858) `eq_empty_of_not_nonempty` gets dropped in favour of `eq_empty_of_is_empty`.

Author

urkud

Parents