mathlib3

e3aca90a - feat(logic/basic): spaces with a zero or a one are nonempty (#2743)

feat(logic/basic): spaces with a zero or a one are nonempty (#2743) Register instances that a space with a zero or a one is not empty, with low priority as we don't want to embark on a search for a zero or a one if this is not necessary. Discussion on Zulip at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/inhabited.20and.20nonempty.20instances/near/198030072 Co-authored-by: Johan Commelin <johan@commelin.net>