Mathlib v3 is deprecated. Go to Mathlib v4

Theorem le_of_mul_le_left

Modification history

2022-10-09 22:10

src/algebra/order/monoid.lean

chore(algebra/order/monoid): split into smaller files (#16861) …

Modified le_of_mul_le_left View on Github →

2022-06-29 18:27

src/algebra/order/monoid.lean

feat(algebra/order/monoid): `a + b ≤ c → a ≤ c` (#15033) …

Added le_of_mul_le_left View on Github →