Commit 2021-11-23 15:06 2b754933

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.