fix: Make rightInverse_inv use RightInverse. (#7792)

fix: Make `rightInverse_inv` use `RightInverse`. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
leanprover-community · Oct 23, 2023 · 16ab7dd · 16ab7dd
1 parent 49b7459
commit 16ab7dd
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
@@ -280,7 +280,7 @@ theorem leftInverse_inv : LeftInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹ :=
 #align left_inverse_neg leftInverse_neg
 
 @[to_additive]
-theorem rightInverse_inv : LeftInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹ :=
+theorem rightInverse_inv : RightInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹ :=
   inv_inv
 #align right_inverse_inv rightInverse_inv
 #align right_inverse_neg rightInverse_neg