Theorem max_mul

Modification history

2024-11-07 16:37
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
chore: generalise `ENNReal` lemmas to `WithTop` (#17786) …
Added max_mulView on Github →