Def IsMax

Modification history

2025-12-03 01:23

Mathlib/Order/Max.lean

feat(Order/Max): use `@[to_dual]` (#32059) …

Deleted IsMax View on Github →

2022-11-18 04:15

Mathlib/Order/Max.lean

feat: port Order.Max (#567) …

Added IsMax View on Github →