Commit 2022-05-07 20:15 e0dd3003

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