mathlib3

0fecc32c - feat(algebra/group_ring_action): add `mul_semiring_action.comp_hom` (#16850)

feat(algebra/group_ring_action): add `mul_semiring_action.comp_hom` (#16850) A multiplicative action of a monoid `M` on a semiring `R` and a monoid homomorphism `N →* M` induce a multiplicative action of a monoid `N` on `R`. I need this for my study of the decomposition and inertia groups Co-authored-by: mkaratarakis <40603357+mkaratarakis@users.noreply.github.com>