Skip to content

[Merged by Bors] - refactor(GroupTheory/GroupAction/Quotient): Move conjugacy class formula earlier#6290

Closed
tb65536 wants to merge 4 commits intomasterfrom
tb_move_conj_classes
Closed

[Merged by Bors] - refactor(GroupTheory/GroupAction/Quotient): Move conjugacy class formula earlier#6290
tb65536 wants to merge 4 commits intomasterfrom
tb_move_conj_classes

Conversation

@tb65536
Copy link
Copy Markdown
Contributor

@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 awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Aug 1, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label 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 labels Aug 8, 2023
@tb65536 tb65536 added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Aug 8, 2023
@j-loreaux
Copy link
Copy Markdown
Contributor

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review 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
Copy Markdown

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
kim-em 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.
kim-em 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.
kim-em 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.
kim-em 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.
kim-em 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.

3 participants