has_inv.inv as a monoid_hom on groups

Stream: Is there code for X?

[Eric Wieser]

We have docs#is_group_hom.inv, but do we have a non-deprecated bundled version somewhere?

[Adam Topaz]

In general (i.e. in the possibly noncommutative case) it's an isomorphism with the opposite group. We should have that as well!

[Eric Wieser]

Ah, we have docs#equiv.inv

[Adam Topaz]

But that says nothing about the group structure

[Eric Wieser]

I know, but it informs me where I should put the lemma - PR incoming :)

[Eric Wieser]

#7330

[Eric Wieser]

Unfortunately we don't have an additive version of opposite, but probably no one cares.