# Commit 2021-04-06 01:49 8e2db7fe

View on Github →refactor(order/boolean_algebra): generalized Boolean algebras (#6775)
We add "generalized Boolean algebras", following a suggestion of @jsm28. Now `boolean_algebra`

extends `generalized_boolean_algebra`

and `boolean_algebra.core`

:

```
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).