mathlib

afad8e43 - refactor(algebra/group_ring_action): split out subobject actions (#17786)

refactor(algebra/group_ring_action): split out subobject actions (#17786) This moves: * Instances for `submonoid` and `subgroup` to a new `algebra.group_ring_action.subobjects` module * Instances for `subsemiring` and `subring` inline with the other smul instances * `invariant_subring` to its own file The argument goes that `mul_semiring_action` is just `mul_distrib_mul_action` + `ring`, so should be available as early as possible in the import hierarchy where both are already available. Cutting out subobject dependencies makes this easier.