Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-09 00:34 bf6e13bf

View on Github →

refactor(algebra/{group,group_with_zero/basic): Generalize lemmas to division monoids (#14000) Generalize group and group_with_zero lemmas to division_monoid. We do not actually delete the original lemmas but make them one-liners from the new ones. The next PR will then delete the old lemmas and perform the renames in all files. Lemmas are renamed because

  • one of the group or group_with_zero name has to go
  • the new API should have a consistent naming convention Pre-emptive lemma renames

Estimated changes

modified theorem div_div
modified theorem div_div_assoc_swap
modified theorem div_div_div_comm
modified theorem div_eq_div_mul_div
modified theorem div_eq_inv_mul'
added theorem div_eq_mul_one_div
modified theorem div_inv_eq_mul
modified theorem div_mul
modified theorem div_ne_one_of_ne
modified theorem div_one'
modified theorem eq_inv_of_mul_eq_one
modified theorem eq_of_div_eq_one'
modified theorem inv_div'
modified theorem inv_div_inv
modified theorem inv_eq_one
modified theorem inv_inv_div_inv
modified theorem inv_mul'
modified theorem inv_mul_eq_div
modified theorem inv_ne_one
modified theorem left_inverse_inv
modified theorem mul_inv
modified theorem one_eq_inv
modified theorem one_inv
added theorem right_inverse_inv
modified theorem div_eq_inv_mul
deleted theorem div_eq_mul_one_div
modified theorem div_one
modified theorem eq_inv_of_mul_left_eq_one
modified theorem eq_inv_of_mul_right_eq_one
modified theorem eq_of_div_eq_one
modified theorem eq_of_one_div_eq_one_div
modified theorem eq_one_div_of_mul_eq_one
modified theorem inv_div
modified theorem inv_div_left
modified theorem inv_eq_one₀
modified theorem inv_one
modified theorem mul_comm_div'
modified theorem mul_inv_rev₀
modified theorem mul_inv₀
modified theorem one_div_div
modified theorem one_div_one
modified theorem one_div_one_div