mathlib
b2ba27ce - move(order/{boolean_algebra → basic}): move `has_compl` and trivial instances (#15602)

Commit
3 years ago
move(order/{boolean_algebra → basic}): move `has_compl` and trivial instances (#15602) We move the trivial `pi.has_sdiff`, `pi.has_compl`, and `Prop.has_compl` instances to `order/basic.lean`. The main effect of this is that `rᶜ` for the complement of a relation is now available basically anywhere.
Author
Parents
Loading