Theorem max_mul

Modification history

2024-12-05 08:47

Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

feat: add `mul_min` and `min_mul` (#18926)

Modified max_mul View on Github →

2024-11-07 16:37

Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

chore: generalise `ENNReal` lemmas to `WithTop` (#17786) …

Added max_mul View on Github →