mathlib

22c4d2ff - feat(order/bounded_order): The lattice of complemented elements (#16267)

feat(order/bounded_order): The lattice of complemented elements (#16267) Define `complementeds`, the subtype of complemented elements, and show that it is a complemented bounded distributive lattice.