Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-02 22:17 41a23769

View on Github →

refactor(algebra/group,group_power): clean up proofs

Estimated changes

Modified algebra/group.lean

modified theorem eq_iff_eq_of_sub_eq_sub

modified theorem eq_iff_sub_eq_zero

modified theorem eq_inv_iff_eq_inv

modified theorem eq_of_mul_inv_eq_one

modified theorem eq_one_of_inv_eq_one

modified theorem eq_sub_iff_add_eq

modified theorem inv_eq_inv_iff_eq

modified theorem inv_eq_one_iff_eq_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_iff_eq_inv_mul

modified theorem mul_eq_iff_eq_mul_inv

modified theorem sub_eq_iff_eq_add

Modified algebra/group_power.lean

deleted theorem gpow_comm

added theorem gpow_mul_comm

modified theorem one_pow

modified theorem pow_add

deleted theorem pow_comm

modified def pow_int

added theorem pow_mul_comm'

added theorem pow_mul_comm

modified def pow_nat

modified theorem pow_succ'

modified theorem pow_succ