mathlib3

f6273d4d - feat(group_theory/group_action/sub_mul_action): Add an object for bundled sets closed under a mul action (#4996)

feat(group_theory/group_action/sub_mul_action): Add an object for bundled sets closed under a mul action (#4996) This adds `sub_mul_action` as a base class for `submodule`, and copies across the relevant lemmas. This also weakens the type class requires for `A →[R] B`, to allow it to be used when only `has_scalar` is available.