Theorem MonotoneOn.mul_strictMono'

Modification history

2024-10-24 21:25

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

feat: use aliases for `CovariantClass α α (· * ·) (· ≤ ·)` etc (#13154)

Modified MonotoneOn.mul_strictMono'View on Github →

2023-01-23 12:02

Mathlib/Algebra/Order/Monoid/Lemmas.lean

chore: tidy various files (#1693)

Added MonotoneOn.mul_strictMono'View on Github →