-
Notifications
You must be signed in to change notification settings - Fork 298
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] - chore(group_theory/specific_groups/*): new folder specific_groups #7018
Conversation
@Julian-Kuelshammer Just to be clear: there is no new material here, right? |
Potential conflict: #6949 |
The only "new material" is the module doc for |
bors merge |
) This creates a new folder `specific_groups` analogous to `analysis.special_functions`. So far, I have put `cyclic` (split from `order_of_element`), `dihedral`, and `quaternion` there. Related Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/group_theory.2Especific_groups
Pull request successfully merged into master. Build succeeded: |
This creates a new folder
specific_groups
analogous toanalysis.special_functions
. So far, I have putcyclic
(split fromorder_of_element
),dihedral
, andquaternion
there.Related Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/group_theory.2Especific_groups