Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 10:36 0d43cc6d

View on Github →

feat(algebra/order/with_zero): Add eq_one_of_mul_eq_one lemmas (#15644)

Estimated changes

Modified src/algebra/order/with_zero.lean

modified theorem div_le_div_left₀

modified theorem div_le_div_right₀

modified theorem div_le_iff₀

added theorem eq_one_of_mul_eq_one_left'

added theorem eq_one_of_mul_eq_one_left

added theorem eq_one_of_mul_eq_one_right'

added theorem eq_one_of_mul_eq_one_right

added theorem inv_le_one₀

modified theorem le_div_iff₀

added theorem mul_le_one₀

added theorem one_le_inv₀

added theorem one_le_mul₀