Commit 2021-12-10 15:16 18ce3a8f

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