-
Notifications
You must be signed in to change notification settings - Fork 299
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(group_theory/group_action/defs): vadd_assoc_class
#15844
Conversation
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.
LGTM
please update to_additive.tr
so that it automatically guesses the correct name (let me know if you need help with that).
bors d+ |
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
I think I got that right? Given that the queue is empty right now, let's give it a try. bors merge |
Additivize `is_scalar_tower` into a new class `vadd_assoc_class`.
Build failed: |
Yep, that works. bors merge |
Additivize `is_scalar_tower` into a new class `vadd_assoc_class`.
Pull request successfully merged into master. Build succeeded: |
vadd_assoc_class
vadd_assoc_class
Additivize
is_scalar_tower
into a new classvadd_assoc_class
.I need this to additivize properly results about
mul_action.stabilizer
that are themselves needed for Kneser's theorem (whose statement is usually given using additive notation, so I really can't do without this).vadd_assoc_class
as a name doesn't really go withis_scalar_tower
(what would?is_add_scalar_assoc_class
?) but it does matchsmul_comm_class
andvadd_comm_class
. I already suggested renamingis_scalar_tower
tosmul_assoc_class
on Zulip, and it would make even more sense after this PR.