Theorem LinearOrder.ext

Modification history

2024-06-08 16:29

Mathlib/Order/Basic.lean

chore(Order/Basic): cleanup redundant type arguments (#13604)

Modified LinearOrder.ext View on Github →

2022-08-18 18:40

Mathlib/Order/Basic.lean

feat(Mathlib/Order/Basic): port most of data/order/basic.lean (#348) …

Added LinearOrder.ext View on Github →