Def DistLat.of

Modification history

2025-02-10 08:46

Mathlib/Order/Category/DistLat.lean

refactor(Order/Category): concrete category refactor for basic orders (#21409) …

Deleted DistLat.of View on Github →

2023-10-17 09:07

Mathlib/Order/Category/DistLat.lean

chore: remove many `Type _` before the colon (#7718) …

Modified DistLat.of View on Github →

2023-09-22 07:38

Mathlib/Order/Category/DistLat.lean

chore: Remove `Cat` suffixes (#3730) …

Added DistLat.of View on Github →