mathlib3

2b754933 - refactor(algebra.group.basic): Convert sub_add_cancel and neg_sub to multaplicative form (#10419)

refactor(algebra.group.basic): Convert sub_add_cancel and neg_sub to multaplicative form (#10419) Currently mathlib has a rich set of lemmas connecting the addition, subtraction and negation additive group operations, but a far thinner collection of results for multiplication, division and inverse multiplicative group operations, despite the fact that the former can be generated easily from the latter via `to_additive`. In #9548 I require multiplicative forms of the existing `sub_add_cancel` and `neg_sub` lemmas. This PR refactors them as the equivalent multiplicative results and then recovers `sub_add_cancel` and `neg_sub` via `to_additive`. There is a complication in that unfortunately `group_with_zero` already has lemmas named `inv_div` and `div_mul_cancel`. I have worked around this by naming the lemmas in this PR `inv_div'` and `div_mul_cancel'` and then manually overriding the names generated by `to_additive`. Other suggestions as to how to approach this welcome.