[Merged by Bors] - feat: primitive group actions#12052
[Merged by Bors] - feat: primitive group actions#12052AntoineChambert-Loir wants to merge 182 commits intomasterfrom
Conversation
Second branch towards the iwasawa criterion We import blocks.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
I wonder whether the hypothesis |
YaelDillies
left a comment
There was a problem hiding this comment.
Yes, that's a good point. You even already made it a class. Do you want to switch over?
|
Does this include all the changes from #12048? |
|
it should. i can't check until tonight |
OK, this LGTM. If all the comments in the other PR have been taken into account let's merge it. bors d+ |
|
✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with |
YaelDillies
left a comment
There was a problem hiding this comment.
Final comments. Thank you for bearing with me!
|
bors r+ |
|
Thank you for your diligence. It's often more work but in the end, it's worth the effort. |
|
Pull request successfully merged into master. Build succeeded: |
This PR defines the notion of a primitive action.
This concept is used to state the Iwasawa criterion for simplicity of #12048