Theorem max_mul

Modification history

2026-08-28 03:45
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
chore(Algebra/Order/Monoid/Unbundled/Basic): golfing + formatting (#38227) …
Modified max_mulView on Github →
2025-08-13 11:43
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
chore(Algebra/Order): replace Co/ContravariantClass by established abbrevs (#28239) …
Modified max_mulView on Github →
2024-12-05 08:47
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
feat: add `mul_min` and `min_mul` (#18926)
Modified max_mulView on Github →
2024-11-07 16:37
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
chore: generalise `ENNReal` lemmas to `WithTop` (#17786) …
Added max_mulView on Github →