Theorem le_of_mul_le_mul_left'
Modification history
2026-08-28 03:45
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
chore(Algebra/Order/Monoid/Unbundled/Basic): golfing + formatting (#38227) …
Modified le_of_mul_le_mul_left'View on Github →2026-04-24 17:35
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
refactor(Algebra/Order/Monoid/Unbundled/Defs): upgrade `*ReflectLE` from `abbrev`s to `class`es (#37393) …
Modified le_of_mul_le_mul_left'View on Github →2024-10-24 21:25
Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
feat: use aliases for `CovariantClass α α (· * ·) (· ≤ ·)` etc (#13154)
Modified le_of_mul_le_mul_left'View on Github →