mathlib3

f068b9de - refactor(algebra/group/basic): Migrate add_comm_group section into comm_group section (#10565)

refactor(algebra/group/basic): Migrate add_comm_group section into comm_group section (#10565) Currently mathlib has a rich set of lemmas connecting the addition, subtraction and negation additive commutative group operations, but a far thinner collection of results for multiplication, division and inverse multiplicative commutative group operations, despite the fact that the former can be generated easily from the latter via to_additive. This PR refactors the additive results in the `add_comm_group` section as the equivalent multiplicative results in the `comm_group` section and then recovers the additive results via to_additive. There is a complication in that unfortunately the multiplicative forms of the names of some of the `add_comm_group` lemmas collide with existing names in `group_with_zero`. I have worked around this by appending an apostrophe to the name and then manually overriding the names generated by to_additive. In a few cases, names with `1...n` appended apostrophes already existed. In these cases I have appended `n+1` apostrophes. Previous discussion The `add_group` section was previously tackled in #10532.