Theorem has_scalar.comp.smul_comm_class'

refactor(algebra/group/defs): rename has_scalar to has_smul (#14559) …

chore(group_theory/group_action/defs): add instances to copy statements about left actions to right actions when the two are equal (#10949) …