Commit 2021-05-25 05:41 d81fcdac

View on Github →

feat(algebra/group_with_zero): add some equational lemmas (#7705) Add some equations for group_with_zero that are direct analogues of lemmas for group. Useful for #6923.

Estimated changes

Modified src/algebra/group_with_zero/basic.lean

added theorem eq_inv_iff

added theorem eq_inv_mul_iff_mul_eq'

modified theorem eq_inv_of_mul_left_eq_one

modified theorem eq_inv_of_mul_right_eq_one

added theorem eq_mul_inv_iff_mul_eq'

modified theorem group_with_zero.mul_left_injective

modified theorem group_with_zero.mul_right_injective

modified theorem inv_eq_iff

modified theorem inv_eq_one'

modified theorem inv_inj'

modified theorem inv_mul_cancel

modified theorem inv_mul_cancel_left'

modified theorem inv_mul_cancel_right'

added theorem inv_mul_eq_iff_eq_mul'

added theorem inv_mul_eq_one'

modified theorem inv_ne_zero

added theorem mul_eq_one_iff_eq_inv'

added theorem mul_eq_one_iff_inv_eq'

modified theorem mul_inv_cancel_left'

modified theorem mul_inv_cancel_right'

added theorem mul_inv_eq_iff_eq_mul'

added theorem mul_inv_eq_one'