Mathlib Changelog
v3
Changelog
About
Github
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
Modified
src/algebra/group/basic.lean
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_div_div_cancel_right'
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_mul_eq_div_div_swap
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'
added
theorem
eq_iff_eq_of_div_eq_div
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_add_right_neg_add
added
theorem
left_inverse_div_mul_left
added
theorem
left_inverse_inv_mul_mul_right
added
theorem
left_inverse_mul_left_div
added
theorem
left_inverse_mul_right_inv_mul
deleted
theorem
left_inverse_neg_add_add_right
deleted
theorem
left_inverse_sub_add_left
added
theorem
mul_div
modified
theorem
mul_div_assoc
added
theorem
mul_div_cancel''
added
theorem
mul_div_mul_right_eq_div
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