has_involutive_inv

Stream: general

[Yury G. Kudryashov]

What do you think about adding a typeclass has_involutive_inv [has_inv G] := (inv_inv : ∀ x : G, (x⁻¹)⁻¹ = x) with instances for group, group_with_zero, pi, and ennreal?

[Eric Wieser]

And has_involutive_neg I assume as well

[Eric Wieser]

Done in #11960, although as extends has_inv G rather than [has_inv G] to match has_involutive_star R.