Commit 2021-09-09 14:10 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) This adds the pointwise actions characterized by ↑(m • S) = (m • ↑S : set R) on:

• submonoid
• subgroup
• add_submonoid
• add_subgroup
• submodule (Zulip)
• subsemiring
• subring
• subalgebra within the locale pointwise (which must be open to state the RHS of the characterization above anyway).