Commit 2022-07-22 18:27 b2ba27ce

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.