mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(algebra/group_ring_action): add `mul_semiring_action.comp_hom`

Open mkaratarakis opened this issue 3 years ago • 5 comments

A multiplicative action of N on R and a ring homomorphism K →+* N induce a multiplicative action of K on R.

I need this for my study of the decomposition and inertia groups

Open in Gitpod

mkaratarakis avatar Oct 07 '22 15:10 mkaratarakis

Lint and build are failing. Could you please fix those?

jcommelin avatar Oct 11 '22 06:10 jcommelin

Thank you. I think these are fixed now - Is there anything else I should do?

mkaratarakis avatar Oct 11 '22 11:10 mkaratarakis

LGTM

Please merge once CI shows a green checkmark

bors d+

fpvandoorn avatar Oct 11 '22 15:10 fpvandoorn

:v: mkaratarakis can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors[bot] avatar Oct 11 '22 15:10 bors[bot]

bors r-

eric-wieser avatar Oct 11 '22 16:10 eric-wieser

OK, thank you. Please let me know if there is anything else

mkaratarakis avatar Oct 15 '22 09:10 mkaratarakis

Also, can you update the PR description? It's no longer accurate

eric-wieser avatar Oct 15 '22 12:10 eric-wieser

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 15 '22 19:10 bors[bot]