Mathlib v3 is deprecated. Go to Mathlib v4

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 bequot 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.

Estimated changes

added inductive free_add_group.red.step
modified theorem free_group.inv_bind
modified theorem free_group.inv_mk
modified theorem free_group.inv_rev_empty
modified theorem free_group.inv_rev_inv_rev
modified theorem free_group.inv_rev_length
modified theorem free_group.lift.mk
modified theorem free_group.lift.of
modified theorem free_group.map.id'
modified theorem free_group.map.id
modified theorem free_group.map.mk
modified theorem free_group.map.of
modified theorem free_group.map_inv
modified theorem free_group.map_mul
modified theorem free_group.map_one
modified theorem free_group.map_pure
modified theorem free_group.mul_bind
modified theorem free_group.mul_mk
modified theorem free_group.norm_eq_zero
modified theorem free_group.norm_inv_eq
modified theorem free_group.norm_one
modified theorem free_group.one_bind
modified theorem free_group.prod.of
modified theorem free_group.prod_mk
modified theorem free_group.pure_bind
modified theorem free_group.quot_lift_mk
modified theorem free_group.quot_lift_on_mk
modified theorem free_group.quot_map_mk
modified theorem free_group.quot_mk_eq_mk
modified theorem free_group.red.refl
modified inductive free_group.red.step
modified theorem free_group.red.trans
modified theorem free_group.red_inv_rev_iff
modified theorem free_group.reduce.cons
deleted theorem free_group.reduce.idem
modified theorem free_group.reduce_to_word
modified theorem free_group.to_word_inj
modified theorem free_group.to_word_mk
modified theorem free_group.to_word_one