mathlib

7c54be86 - feat(group_theory/group_action/sub_mul_action): add the pointwise monoid structure (#15050)