Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-17 10:43 614758eb

View on Github →

feat(order/category/DistribLattice): The category of distributive lattices (#12092) Define DistribLattice, the category of distributive lattices.

Estimated changes

Created src/order/category/DistribLattice.lean

added def DistribLattice.dual

added def DistribLattice.dual_equiv

added def DistribLattice.iso.mk

added def DistribLattice.of

added def DistribLattice

added theorem DistribLattice_dual_comp_forget_to_Lattice

Modified src/order/category/Lattice.lean