mathlib

2331607e - feat(group_theory/sub{monoid,group}): pointwise actions on `add_sub{monoid,group}`s and `sub{monoid,group,module,semiring,ring,algebra}`s (#8945)

feat(group_theory/sub{monoid,group}): pointwise actions on `add_sub{monoid,group}`s and `sub{monoid,group,module,semiring,ring,algebra}`s (#8945) This adds the pointwise actions characterized by `↑(m • S) = (m • ↑S : set R)` on: * `submonoid` * `subgroup` * `add_submonoid` * `add_subgroup` * `submodule` ([Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lost.20instance/near/249467913)) * `subsemiring` * `subring` * `subalgebra` within the locale `pointwise` (which must be open to state the RHS of the characterization above anyway).