Skip to content
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] - refactor(GroupTheory/GroupAction/Quotient): Move conjugacy class formula earlier #6290

Closed
wants to merge 4 commits into from

Conversation

tb65536
Copy link
Collaborator

@tb65536 tb65536 commented Aug 1, 2023

This PR moves a formula for the number of conjugacy classes earlier. The proof uses Burnside's theorem, so it cannot be moved any earlier than GroupTheory/GroupAction/Quotient.


Open in Gitpod

@tb65536 tb65536 added awaiting-review The author would like community review of the PR awaiting-CI t-algebra Algebra (groups, rings, fields etc) labels Aug 1, 2023
@j-loreaux j-loreaux added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Aug 8, 2023
@tb65536 tb65536 added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 8, 2023
@j-loreaux
Copy link
Collaborator

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Aug 9, 2023
bors bot pushed a commit that referenced this pull request Aug 9, 2023
…ula earlier (#6290)

This PR moves a formula for the number of conjugacy classes earlier. The proof uses Burnside's theorem, so it cannot be moved any earlier than `GroupTheory/GroupAction/Quotient`.
@bors
Copy link

bors bot commented Aug 9, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title refactor(GroupTheory/GroupAction/Quotient): Move conjugacy class formula earlier [Merged by Bors] - refactor(GroupTheory/GroupAction/Quotient): Move conjugacy class formula earlier Aug 9, 2023
@bors bors bot closed this Aug 9, 2023
@bors bors bot deleted the tb_move_conj_classes branch August 9, 2023 19:01
semorrison pushed a commit that referenced this pull request Aug 14, 2023
…ula earlier (#6290)

This PR moves a formula for the number of conjugacy classes earlier. The proof uses Burnside's theorem, so it cannot be moved any earlier than `GroupTheory/GroupAction/Quotient`.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
semorrison pushed a commit that referenced this pull request Aug 15, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
semorrison pushed a commit that referenced this pull request Aug 15, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
semorrison pushed a commit that referenced this pull request Aug 15, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
semorrison pushed a commit that referenced this pull request Aug 17, 2023
This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants