mathlib

84d27b45 - refactor(group_theory/group_action/defs): generalize smul_mul_assoc and mul_smul_comm (#7441)

refactor(group_theory/group_action/defs): generalize smul_mul_assoc and mul_smul_comm (#7441) These lemmas did not need a full algebra structure; written this way, it permits usage on `has_scalar (units R) A` given `algebra R A` (in some future PR). For now, the old algebra lemmas are left behind, to minimize the scope of this patch.