mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

chore(specific_groups/cyclic): add `@[to_additive]` to cyclic group

Open jamesa9283 opened this issue 4 years ago • 1 comments

Add @[to_additive] to cyclic group and amend documentation.

  • adds @[to_additive] to the cyclic group.
  • amends documentation with more accurate defintion.

Open in Gitpod

jamesa9283 avatar Sep 08 '21 21:09 jamesa9283

You also need to add @[to_additive] to all the other declarations. Ideally we could tweak the implementation of to_additive so that it automatically replaces cyclic with cyclic_add in name fragments, so that you don't have to specify all the new names by hand.

kim-em avatar Sep 09 '21 06:09 kim-em