[Merged by Bors] - feat(algebra/group_ring_action) define group actions on rings #2566
Conversation
src/algebra/group_ring_action.lean
Outdated
| (smul_mul : ∀ (g : α) (x y : β), g • (x * y) = (g • x) * (g • y)) | ||
|
|
||
| /-- Typeclass for multiplicative actions by monoids on additive monoids. -/ | ||
| class mul_add_action [monoid α] [add_monoid β] extends mul_action α β := |
There was a problem hiding this comment.
This already exists under the name distrib_mul_action
There was a problem hiding this comment.
Should I keep the to_additive?
There was a problem hiding this comment.
BTW, could you please use descriptive type variable names? E.g., M for a monoid and R for a ring. We should add this to naming.md. And there should be an instance for algebra being a mul_semiring_action.
Note that we have an incompatible idea of what is a good class for a ring action on a ring in ring_theory/algebra, and some lemmas (e.g., smul_one) make sense for both of them (and also for the left action of a non-commutative semiring on itself), so we should be careful about lemma names.
|
@kckennylau If you can make the linter happy, feel free to make bors happy afterwards (-; bors defer |
|
bors d+ |
|
✌️ kckennylau can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
Define group action on rings. Related Zulip discussions: - https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.232566.20group.20actions.20on.20ring - https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mul_action
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…over-community#2566) Define group action on rings. Related Zulip discussions: - https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.232566.20group.20actions.20on.20ring - https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mul_action
…over-community#2566) Define group action on rings. Related Zulip discussions: - https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.232566.20group.20actions.20on.20ring - https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mul_action
…over-community#2566) Define group action on rings. Related Zulip discussions: - https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.232566.20group.20actions.20on.20ring - https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mul_action
Define group action on rings.
Related Zulip discussions:
TO CONTRIBUTORS:
Please include a summary of the changes made in this PR above "TO CONTRIBUTORS:", as that text will become the commit message. You are also encouraged to append the following co-authorship template if you'd like to acknowledge suggestions / commits made by other users:
Co-authored-by: name name@example.com
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list
If you're confused by comments on your PR like
bors r+orbors d+, please see our notes on bors for information on our merging workflow.