Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-01 01:58 73f95a7a

View on Github →

chore(algebra/group): move defs to defs.lean (#2885) Also delete the aliases eq_of_add_eq_add_left and eq_of_add_eq_add_right.

Estimated changes

deleted theorem group.mul_left_cancel
deleted theorem group.mul_right_cancel
deleted theorem inv_eq_of_mul_eq_one
deleted theorem inv_inv
deleted theorem inv_mul_cancel_left
deleted def inv_mul_self
deleted theorem left_inv_eq_right_inv
deleted theorem mul_assoc
deleted theorem mul_comm
deleted theorem mul_inv_cancel_right
deleted def mul_inv_self
deleted theorem mul_left_cancel
deleted theorem mul_left_cancel_iff
deleted theorem mul_left_inj
deleted theorem mul_left_injective
deleted theorem mul_left_inv
deleted theorem mul_one
deleted theorem mul_right_cancel
deleted theorem mul_right_cancel_iff
deleted theorem mul_right_inj
deleted theorem mul_right_injective
deleted theorem mul_right_inv
deleted theorem one_mul
deleted theorem sub_eq_add_neg
added theorem inv_eq_of_mul_eq_one
added theorem inv_inv
added theorem inv_mul_cancel_left
added theorem inv_mul_self
added theorem left_inv_eq_right_inv
added theorem mul_assoc
added theorem mul_comm
added theorem mul_inv_cancel_right
added theorem mul_inv_self
added theorem mul_left_cancel
added theorem mul_left_cancel_iff
added theorem mul_left_inj
added theorem mul_left_injective
added theorem mul_left_inv
added theorem mul_one
added theorem mul_right_cancel
added theorem mul_right_cancel_iff
added theorem mul_right_inj
added theorem mul_right_injective
added theorem mul_right_inv
added theorem one_mul
added theorem sub_eq_add_neg