mathlib
49b8b91a - feat(data/fintype/order): `bool` is a boolean algebra (#11694)

Commit
3 years ago
feat(data/fintype/order): `bool` is a boolean algebra (#11694) Provide the `boolean_algebra` instance for `bool` and use the machinery from `data.fintype.order` to deduce `complete_boolean_algebra bool` and `complete_linear_order bool`.
Author
Parents
Loading