Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-06 06:59 dc6adcc8

View on Github →

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.

Estimated changes