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

This means expressions like `has_inv.inv ∘ has_inv.inv` can be simplified





leanprover-community/mathlib,leanprover-community/mathlib