Improved notation for inverses and units in groups

[mikeshulman]

As discussed at #1155, it would be nice to be able to write something like x^-1 instead of - x for inverses in a multiplicative group (i.e. a group with mc_mult_scope opened). (There's probably no need to have anything similar for Mult instances, since those are generally used for rings and the multiplicative monoid of a ring is never nontrivially a group, instead we have Recip for inverting nonzero elements in fields.)

It would also be nice to be able to use 0 and 1 for the unit elements in additive and multiplicative monoids respectively.

[Alizter]

Would it be sensible to use x^ for inverses, since it is more economical to type. We can probably set this up without affecting our notation for paths.

[mikeshulman]

Perhaps.

(I think you mean "affecting".)