mathlib3

b5925894 - refactor(order/boolean_algebra): factor out pi.sdiff and pi.compl (#9955)

refactor(order/boolean_algebra): factor out pi.sdiff and pi.compl (#9955) Provide definitional lemmas about sdiff and compl on pi types. This allows usage later on even without a whole `boolean_algebra` instance.