mathlib3

18ce3a8f - feat(group_theory/group_action/defs): add a typeclass to show that an action is central (aka symmetric) (#10543)

feat(group_theory/group_action/defs): add a typeclass to show that an action is central (aka symmetric) (#10543) This adds a new `is_central_scalar` typeclass to indicate that `op m • a = m • a` (or rather, to indicate that a type has the same right and left scalar action on another type). The main instance for this is `comm_semigroup.is_central_scalar`, for when `m • a = m * a` and `op m • a = a * m`, and then all the other instances follow transitively when `has_scalar R (f M)` is derived from `has_scalar R M`: * `prod` * `pi` * `ulift` * `finsupp` * `dfinsupp` * `monoid_algebra` * `add_monoid_algebra` * `polynomial` * `mv_polynomial` * `matrix` * `add_monoid_hom` * `linear_map` * `complex` * `pointwise` instances on: * `set` * `submonoid` * `add_submonoid` * `subgroup` * `add_subgroup` * `subsemiring` * `subring` * `submodule`