We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent cc016b6 commit 571a128Copy full SHA for 571a128
Mathlib/Algebra/Group/Basic.lean
@@ -252,7 +252,7 @@ theorem inv_injective : Function.Injective (Inv.inv : G → G) :=
252
#align neg_injective neg_injective
253
254
@[to_additive (attr := simp)]
255
-theorem inv_inj {a b : G} : a⁻¹ = b⁻¹ ↔ a = b :=
+theorem inv_inj : a⁻¹ = b⁻¹ ↔ a = b :=
256
inv_injective.eq_iff
257
#align inv_inj inv_inj
258
#align neg_inj neg_inj
0 commit comments