Def Lattice.of

Modification history

2023-03-28 23:45

src/order/category/Lattice.lean

chore(order/category): Rename categories (#18657) …

Deleted Lattice.of View on Github →

2022-02-15 14:39

src/order/category/Lattice.lean

feat(order/category/Lattice): The category of lattices (#11968) …

Added Lattice.of View on Github →