Commit 2020-12-22 03:10 3c7394fe

fix(group_theory/*, algebra/group): [to_additive, simp] doesn't work (#5468) As explained in algebra/group/to_additive, @[to_additive, simp] doesn't work (it doesn't attach a simp attribute to the additive lemma), but conversely @[simps, to_additive] is also wrong. Along the way I also noticed that some right_inv (as in an inverse function) lemmas were being changed to right_neg by to_additive :D