Def Lattice.toLinearOrder

Modification history

2024-05-07 01:05

Mathlib/Order/Lattice.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted Lattice.toLinearOrder View on Github →

2022-11-25 17:46

Mathlib/Order/Lattice.lean

feat: port Order.Lattice (#642) …

Added Lattice.toLinearOrder View on Github →