Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-02-15 09:59
0b6d398e
View on Github →
chore(algebra/group/basic): rename type vars (
#1989
)
Estimated changes
Modified
src/algebra/group/basic.lean
modified
theorem
add_add_neg_cancel'_right
modified
theorem
add_add_sub_cancel
modified
theorem
add_sub_cancel'
modified
theorem
add_sub_cancel'_right
modified
theorem
add_sub_sub_cancel
modified
theorem
bit0_zero
modified
theorem
bit1_zero
modified
theorem
eq_iff_eq_of_sub_eq_sub
modified
theorem
eq_inv_iff_eq_inv
modified
theorem
eq_inv_iff_mul_eq_one
modified
theorem
eq_inv_mul_iff_mul_eq
modified
theorem
eq_mul_inv_iff_mul_eq
modified
theorem
eq_of_inv_eq_inv
modified
theorem
eq_sub_iff_add_eq'
modified
theorem
eq_sub_iff_add_eq
modified
theorem
inv_comm_of_comm
modified
theorem
inv_eq_iff_inv_eq
modified
theorem
inv_eq_iff_mul_eq_one
modified
theorem
inv_eq_one
modified
theorem
inv_inj'
modified
theorem
inv_mul_eq_iff_eq_mul
modified
theorem
inv_ne_one
modified
theorem
left_inverse_add_left_sub
modified
theorem
left_inverse_add_right_neg_add
modified
theorem
left_inverse_inv
modified
theorem
left_inverse_neg_add_add_right
modified
theorem
left_inverse_sub_add_left
modified
theorem
mul_eq_one_iff_eq_inv
modified
theorem
mul_eq_one_iff_inv_eq
modified
theorem
mul_inv_eq_iff_eq_mul
modified
theorem
mul_inv_eq_one
modified
theorem
mul_left_inj
modified
theorem
mul_left_injective
modified
theorem
mul_left_surjective
modified
theorem
mul_mul_mul_comm
modified
theorem
mul_right_inj
modified
theorem
mul_right_injective
modified
theorem
mul_right_surjective
modified
theorem
mul_self_iff_eq_one
modified
theorem
neg_add'
modified
theorem
neg_sub_neg
modified
theorem
sub_add_add_cancel
modified
theorem
sub_add_sub_cancel'
modified
theorem
sub_add_sub_cancel
modified
theorem
sub_eq_iff_eq_add'
modified
theorem
sub_eq_iff_eq_add
modified
theorem
sub_eq_neg_add
modified
theorem
sub_eq_sub_iff_sub_eq_sub
modified
theorem
sub_eq_zero
modified
theorem
sub_left_inj
modified
theorem
sub_ne_zero
modified
theorem
sub_right_comm
modified
theorem
sub_right_inj
modified
theorem
sub_sub_assoc_swap
modified
theorem
sub_sub_cancel
modified
theorem
sub_sub_sub_cancel_left
modified
theorem
sub_sub_sub_cancel_right