mathlib

dc6adcc8 - feat(order/bounded_lattice): define the `distrib_lattice_bot` typeclass (#8507)

feat(order/bounded_lattice): define the `distrib_lattice_bot` typeclass (#8507) Typeclass for a distributive lattice with a least element. This typeclass is used to generalize `disjoint_sup_left` and similar. It inserts itself in the hierarchy between `semilattice_sup_bot, semilattice_inf_bot` and `generalized_boolean_algebra`, `bounded_distrib_lattice`. I am doing it through `extends`.