Def minDefault

Modification history

2024-11-26 10:41

Mathlib/Order/Defs.lean

chore: split Order.Defs (#19498)

Modified minDefault View on Github →

2024-09-14 05:31

Mathlib/Order/Defs.lean

chore: tidy/move/deprecate `Init.Logic` and `IsSymmOp` more (#16757) …

Modified minDefault View on Github →

2022-11-25 17:46

Mathlib/Init/Algebra/Order.lean

feat: port Order.Lattice (#642) …

Added minDefault View on Github →