Commit 2019-12-13 22:04 a3844c85

View on Github →

chore(algebra/group/basic): DRY, add mul_left_surjective (#1801) Some lemmas explicitly listed arguments already declared using variables, remove them.

Estimated changes

Modified src/algebra/group/basic.lean

modified theorem inv_comm_of_comm

modified theorem mul_inv_eq_one

modified theorem mul_left_eq_self

added theorem mul_left_surjective

modified theorem mul_right_eq_self

added theorem mul_right_surjective