Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 14:55 34ce7847

View on Github →

refactor(algebra/group_with_zero/basic): Golf using division monoid lemmas (#14213) Make all eligible group_with_zero lemmas one-liners from division_monoid ones and group them within the file.

Estimated changes

modified theorem div_div_cancel'
modified theorem div_eq_iff
modified theorem div_eq_iff_mul_eq
modified theorem div_eq_of_eq_mul
modified theorem div_eq_one_iff_eq
modified theorem div_helper
modified theorem div_left_inj'
modified theorem div_mul_cancel
modified theorem div_mul_left
modified theorem div_mul_right
modified theorem div_self
modified theorem eq_div_iff
modified theorem eq_div_iff_mul_eq
modified theorem eq_div_of_mul_eq
modified theorem inv_mul_eq_one₀
modified theorem is_unit_iff_ne_zero
modified theorem mul_div_cancel'
modified theorem mul_div_cancel
modified theorem mul_div_cancel_left
modified theorem mul_div_mul_left
modified theorem mul_div_mul_right
modified theorem mul_eq_one_iff_eq_inv₀
modified theorem mul_eq_one_iff_inv_eq₀
modified theorem mul_inv_eq_one₀
modified theorem mul_left_inj'
modified theorem mul_mul_div
modified theorem mul_one_div_cancel
modified theorem mul_right_inj'
modified theorem one_div_mul_cancel