learnlean

Did the final three exercises in the Proving Identities in Algebraic Structures section. These involved proving theorems about groups using only the group axioms. 

Normally multiplying by the inverse is defined to be commutative in text books, but not here. So the first task was proving that fact. I had to look up the helper lemma for `mul_inv_cancel`, but after that proving the lemma and the theorem + `mul_one` was easy (see pic 1).

The last exercise was proving `(a * b)⁻¹ = b⁻¹ * a⁻¹`. This I'm rather proud of, because I think my solution is more legible than the official one (see pic 2).

Great work on tackling those group theory exercises! Your approach to `(a * b)⁻¹ = b⁻¹ * a⁻¹` sounds intriguing. Would love to see how your solution compares to the official one!