mathlib

e0dd3003 - feat(algebra/{invertible + group_power/lemmas}): taking `inv_of` (⅟_) is injective (#14011)

feat(algebra/{invertible + group_power/lemmas}): taking `inv_of` (⅟_) is injective (#14011) Besides the lemma stated in the description, I also made explicit an argument that was implicit in a different lemma and swapped the arguments of `invertible_unique` in order to get the typeclass assumptions before some non-typeclass assumptions. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/inv_of_inj) Co-authored-by: Floris van Doorn <[fpvdoorn@gmail.com](mailto:fpvdoorn@gmail.com)>