Commit 2022-04-05 09:11 ea1917b6

feat(algebra/group/to_additive + algebra/regular/basic): add to_additive for is_regular (#12930) This PR add the to_additive attribute to most lemmas in the file algebra.regular.basic. I also added to_additive support for this: to_additive converts

• is_regular to is_add_regular;
• is_left_regular to is_add_left_regular;
• is_right_regular to is_add_right_regular. Currently, to_additive converts regular to add_regular. This means that, for instance, is_left_regular becomes is_left_add_regular. I have a slight preference for is_add_left_regular/is_add_right_regular, but I am not able to achieve this automatically. EDIT: actually, the command

git ls-files | xargs grep -A1 "to\_additive" | grep -B1 regular

reveals more name changed by to_additive that require more thought.