Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-30 15:07 8bce7eb0

View on Github →

refactor(algebra/group/basic): Migrate add_group section into group section (#10532)

Estimated changes

deleted theorem add_eq_of_eq_sub
deleted theorem add_sub
deleted theorem add_sub_add_right_eq_sub
deleted theorem add_sub_assoc
deleted theorem add_sub_cancel
added theorem div_div_assoc_swap
added theorem div_eq_iff_eq_mul
added theorem div_eq_of_eq_mul''
added theorem div_eq_one
added theorem div_eq_self
added theorem div_inv_eq_mul
added theorem div_left_inj
added theorem div_mul_div_cancel'
added theorem div_ne_one
added theorem div_ne_one_of_ne
added theorem div_right_inj
added theorem div_self'
deleted theorem eq_add_of_sub_eq
added theorem eq_div_iff_mul_eq'
added theorem eq_div_of_mul_eq'
deleted theorem eq_iff_eq_of_sub_eq_sub
added theorem eq_mul_of_div_eq
added theorem eq_of_div_eq_one'
deleted theorem eq_of_sub_eq_zero
deleted theorem eq_sub_iff_add_eq
deleted theorem eq_sub_of_add_eq
deleted theorem left_inverse_add_left_sub
deleted theorem left_inverse_sub_add_left
added theorem mul_div
modified theorem mul_div_assoc
added theorem mul_div_cancel''
added theorem mul_eq_of_eq_div
deleted theorem sub_add_eq_sub_sub_swap
deleted theorem sub_add_sub_cancel
deleted theorem sub_eq_iff_eq_add
deleted theorem sub_eq_of_eq_add
deleted theorem sub_eq_self
deleted theorem sub_eq_zero
deleted theorem sub_left_inj
deleted theorem sub_ne_zero
deleted theorem sub_ne_zero_of_ne
deleted theorem sub_neg_eq_add
deleted theorem sub_right_inj
deleted theorem sub_self
deleted theorem sub_sub_assoc_swap
deleted theorem sub_sub_sub_cancel_right