Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-10 17:00 3ea573ef

View on Github →

refactor(algebra/{group,group_with_zero/basic): Delete lemmas generalized to division monoids (#14042) Delete the group and group_with_zero lemmas which have been made one-liners in #14000. 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 Lemma renames

Estimated changes

modified theorem div_div
deleted theorem div_div_assoc_swap
modified theorem div_div_div_comm
added theorem div_div_div_eq
added theorem div_div_eq_mul_div
deleted theorem div_eq_inv_mul'
added theorem div_eq_inv_mul
modified theorem div_inv_eq_mul
modified theorem div_mul
added theorem div_mul_comm
modified theorem div_mul_div_comm
modified theorem div_mul_eq_div_div
modified theorem div_mul_eq_div_div_swap
deleted theorem div_mul_eq_mul_div'
added theorem div_mul_eq_mul_div
modified theorem div_ne_one_of_ne
deleted theorem div_one'
added theorem div_one
deleted theorem div_right_comm'
added theorem div_right_comm
deleted theorem division_monoid.div_one
deleted theorem division_monoid.inv_div
deleted theorem division_monoid.inv_one
deleted theorem eq_inv_of_mul_eq_one
deleted theorem eq_of_div_eq_one'
added theorem eq_of_div_eq_one
modified theorem inv_div'
added theorem inv_div
modified theorem inv_div_inv
added theorem inv_div_left
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
added theorem inv_one
added theorem mul_comm_div
modified theorem mul_div
modified theorem mul_div_cancel'''
deleted theorem mul_div_comm'
modified theorem mul_div_left_comm
added theorem mul_div_mul_comm
added theorem mul_div_right_comm
modified theorem mul_inv
added theorem one_div_div
added theorem one_div_mul_one_div
added theorem one_div_one
added theorem one_div_one_div
modified theorem one_eq_inv
deleted theorem one_inv
deleted theorem inv_eq_of_mul_eq_one
deleted theorem div_div_div_comm₀
deleted theorem div_div_div_div_eq
deleted theorem div_div_eq_div_mul
deleted theorem div_div_eq_mul_div
deleted theorem div_eq_inv_mul
deleted theorem div_mul_comm'
deleted theorem div_mul_div_comm₀
deleted theorem div_mul_eq_mul_div
deleted theorem div_mul_eq_mul_div_comm
deleted theorem div_one
deleted theorem div_right_comm
deleted theorem eq_inv_of_mul_left_eq_one
deleted theorem eq_of_div_eq_one
deleted theorem eq_of_one_div_eq_one_div
deleted theorem eq_one_div_of_mul_eq_one
deleted theorem inv_div
deleted theorem inv_div_left
deleted theorem inv_eq_one₀
deleted theorem inv_one
deleted theorem mul_comm_div'
deleted theorem mul_div_comm
deleted theorem mul_div_right_comm
modified theorem mul_eq_mul_of_div_eq_div
deleted theorem mul_inv_rev₀
deleted theorem mul_inv₀
deleted theorem one_div_div
deleted theorem one_div_mul_one_div
deleted theorem one_div_mul_one_div_rev
deleted theorem one_div_one
deleted theorem one_div_one_div
deleted theorem is_add_group_hom.map_sub
added theorem is_group_hom.map_div
modified theorem alternating_map.map_swap
deleted theorem fractional_ideal.one_inv
deleted theorem mv_power_series.one_inv
added theorem power_series.inv_one
deleted theorem power_series.one_inv
modified theorem tactic.abel.unfold_sub