Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi.compl_def

Modification history

2022-07-22 18:27
src/order/basic.lean
move(order/{boolean_algebra → basic}): move `has_compl` and trivial instances (#15602) …
Modified pi.compl_defView on Github →
2021-10-26 22:41
src/order/boolean_algebra.lean
refactor(order/boolean_algebra): factor out pi.sdiff and pi.compl (#9955) …
Added pi.compl_defView on Github →