Commit 2021-12-11 19:31 f068b9de

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.