chore(algebra/group/basic): Mark inv_involutive simp (#4744)

This means expressions like `has_inv.inv ∘ has_inv.inv` can be simplified
leanprover-community · Oct 23, 2020 · 458c833 · 458c833
1 parent bb52355
commit 458c833
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/algebra/group/basic.lean b/src/algebra/group/basic.lean
@@ -95,7 +95,7 @@ theorem left_inverse_inv (G) [group G] :
   function.left_inverse (λ a : G, a⁻¹) (λ a, a⁻¹) :=
 inv_inv
 
-@[to_additive]
+@[simp, to_additive]
 lemma inv_involutive : function.involutive (has_inv.inv : G → G) := inv_inv
 
 @[to_additive]