mathlib3

8e2db7fe - refactor(order/boolean_algebra): generalized Boolean algebras (#6775)

refactor(order/boolean_algebra): generalized Boolean algebras (#6775) We add ["generalized Boolean algebras"](https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Generalizations), following a [suggestion](https://github.com/leanprover-community/mathlib/pull/6469#issuecomment-787521935) of @jsm28. Now `boolean_algebra` extends `generalized_boolean_algebra` and `boolean_algebra.core`: ```lean class generalized_boolean_algebra (α : Type u) extends semilattice_sup_bot α, semilattice_inf_bot α, distrib_lattice α, has_sdiff α := (sup_inf_sdiff : ∀a b:α, (a ⊓ b) ⊔ (a \ b) = a) (inf_inf_sdiff : ∀a b:α, (a ⊓ b) ⊓ (a \ b) = ⊥) class boolean_algebra.core (α : Type u) extends bounded_distrib_lattice α, has_compl α := (inf_compl_le_bot : ∀x:α, x ⊓ xᶜ ≤ ⊥) (top_le_sup_compl : ∀x:α, ⊤ ≤ x ⊔ xᶜ) class boolean_algebra (α : Type u) extends generalized_boolean_algebra α, boolean_algebra.core α := (sdiff_eq : ∀x y:α, x \ y = x ⊓ yᶜ) ``` I also added a module doc for `order/boolean_algebra`. Many lemmas about set difference both for `finset`s and `set`s now follow from their `generalized_boolean_algebra` counterparts and I've removed the (fin)set-specific proofs. `finset.sdiff_subset_self` was removed in favor of the near-duplicate `finset.sdiff_subset` (the latter has more explicit arguments).