Theorem max_commutative

Modification history

2024-10-15 23:21

Mathlib/Deprecated/MinMax.lean

chore: move `Init.Logic` and its remaining dependencies to `Deprecated` (#17771) …

Modified max_commutative View on Github →

2024-09-13 04:26

Mathlib/Order/MinMax.lean

chore: deprecate plain `Commutative, Associative` (#16749) …

Modified max_commutative View on Github →

2022-11-26 03:55

Mathlib/Order/MinMax.lean

feat: port order.minmax (#728) …

Added max_commutative View on Github →