Commit 2021-08-23 14:22 df3e8862

feat(group_theory/group_action): generalize mul_action.function_End to other endomorphisms (#8724) The main aim of this PR is to remove intermediate_field.subgroup_action which is a weird special case of the much more general instance f • a = f a, added in this PR as alg_equiv.apply_mul_semiring_action. We add the same actions for all the other hom types for consistency. These generalizations are in line with the mul_action.function_End (renamed to function.End.apply_mul_action) and mul_action.perm (renamed to equiv.perm.apply_mul_action) instances introduced by @dwarn, providing any endomorphism that has a monoid structure with a faithful mul_action corresponding to function application. Note that there is no monoid structure on ring_equiv, or alg_hom, so this PR does not bother with the corresponding action.