Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eq_one_of_mul_eq_one_left

Modification history

2022-08-29 08:18
src/algebra/order/with_zero.lean
refactor(algebra/order/with_zero): Generalize lemmas (#16240) …
Deleted eq_one_of_mul_eq_one_leftView on Github →
2022-08-16 10:36
src/algebra/order/with_zero.lean
feat(algebra/order/with_zero): Add eq_one_of_mul_eq_one lemmas (#15644)
Added eq_one_of_mul_eq_one_leftView on Github →