Commit 2022-11-15 05:54 a22318f3
View on Github →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.redon 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.