Def CompleteLat.of

Modification history

2025-02-19 20:44

Mathlib/Order/Category/CompleteLat.lean

feat(Order/Category): `ConcreteCategory` instance for `CompleteLat` (#21410) …

Deleted CompleteLat.of View on Github →

2023-09-22 07:38

Mathlib/Order/Category/CompleteLat.lean

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

Added CompleteLat.of View on Github →