Commit 2021-05-05 18:50 84d27b45
View on Github →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.