mathlib3

a22318f3 - feat(group_theory/free_group): to_additivize where possible (#17034)

feat(group_theory/free_group): to_additivize where possible (#17034) For some applications of #2819 I'd like to have additive versions of some results proved using `free_group`, but unfortunately there is no `free_add_group`, so we rectify this here by to_additivizing the file `free_group. This is done in a rather clumsy way here, making a separate relation `free_add_group.red` on words (lists of elements x bool), even though it is of course the same relation for additive and multiplicative groups when thought of as a relation on lists, and then using to_additive on everything in the file (even if its the same in both cases). The reason for this is that having the same relation for the additive and multiplicative version causes both types to be `quot red`, so simp gets all messed up when defining simp lemmas turning elements of that type into `mk blah`. So, while a more elegant way is probably possible, it seems rather tricky to set up compared to the approach in this PR. There are a couple of places where `to_additive` doesn't work, either because the situation is too complicated, or a bug in to additive (it seems). For now we just ignore those small sections. A couple of small proof golfs/typos are also fixed in the file.