Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eq_one_of_mul_le_one_left

Modification history

2022-08-29 08:18
src/algebra/order/monoid_lemmas.lean
refactor(algebra/order/with_zero): Generalize lemmas (#16240) …
Added eq_one_of_mul_le_one_leftView on Github →