Theorem PUnit.min_eq

Modification history

2025-12-02 12:55

Mathlib/Order/Basic.lean

chore(Order/Basic): use `@[to_dual]` (#31903) …

Deleted PUnit.min_eq View on Github →

2023-06-25 11:21

Mathlib/Order/Basic.lean

chore: disable relaxedAutoImplicit (#5277) …

Modified PUnit.min_eq View on Github →

2022-11-14 11:36

Mathlib/Order/Basic.lean

feat: port Order.Basic (#556) …

Added PUnit.min_eq View on Github →