New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(to_additive + Cyclic): auto cyclic --> addCyclic
#8722
Conversation
Thanks! maintainer merge |
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
Thanks! |
Teach the conversion `Cyclic ↦ addCyclic` to `to_additive`. Affected files: ```bash GroupTheory/SpecificGroups/Cyclic Tactic/ToAdditive ```
Cyclic --> addCyclic
cyclic --> addCyclic
@adomani, is there a reason you've taken to listing the affected files in the commit message? This is tracked automatically by git, so seems redundant (and therefore at risk of being wrong) to me. |
Eric, I removed the affected files in this PR. I have a script that creates (a template for) the commit message and had it in there. I'll get rid of it! |
Pull request successfully merged into master. Build succeeded: |
cyclic --> addCyclic
cyclic --> addCyclic
Teach the conversion `Cyclic ↦ addCyclic` to `to_additive`. Affected files: ```bash GroupTheory/SpecificGroups/Cyclic Tactic/ToAdditive ```
Teach the conversion
Cyclic ↦ addCyclic
toto_additive
.