-
Notifications
You must be signed in to change notification settings - Fork 234
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: Compare card of subgroup to card of group #5347
Conversation
Maintainers, let me know if we are not accepting PRs to ported files yet |
new results are fine to add (maybe not new instances, depending on the situation), but refactors will probably be forced to wait until after the port. Also, just FYI, we no longer specify the filename in the PR title. |
Ok cool no refactors here, just new lemmas |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks: please apply the suggestion and then feel free to merge.
bors d+
Co-authored-by: Oliver Nash <github@olivernash.org>
bors merge |
Includes new lemmas, one that shows that the cardinality of a subgroup is at most the cardinality of the ambient group, and others which shows that the cardinality of the top group is equal to that of the ambient group, and that in fact this is iff. Co-authored-by: Floris van Doorn
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Includes new lemmas, one that shows that the cardinality of a subgroup is at most the cardinality of the ambient group, and others which shows that the cardinality of the top group is equal to that of the ambient group, and that in fact this is iff. Co-authored-by: Floris van Doorn
Includes new lemmas, one that shows that the cardinality of a subgroup is at most the cardinality of the ambient group, and others which shows that the cardinality of the top group is equal to that of the ambient group, and that in fact this is iff. Co-authored-by: Floris van Doorn
Includes new lemmas, one that shows that the cardinality of a subgroup is at most the cardinality of the ambient group, and others which shows that the cardinality of the top group is equal to that of the ambient group, and that in fact this is iff.
Co-authored-by: Floris van Doorn