Commit 2022-03-28 20:38 ea97ca6b
View on Github →feat(group_theory/group_action): add commute.smul_{left,right}[_iff] lemmas (#13003)
(r • a) * b = b * (r • a) follows trivially from smul_mul_assoc and mul_smul_comm
feat(group_theory/group_action): add commute.smul_{left,right}[_iff] lemmas (#13003)
(r • a) * b = b * (r • a) follows trivially from smul_mul_assoc and mul_smul_comm