mathlib3
ea97ca6b - feat(group_theory/group_action): add `commute.smul_{left,right}[_iff]` lemmas (#13003)

Commit

3 years ago

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`

Author

eric-wieser

Parents

261a1953

mathlib3 ea97ca6b - feat(group_theory/group_action): add `commute.smul_{left,right}[_iff]` lemmas (#13003)

mathlib3
ea97ca6b - feat(group_theory/group_action): add `commute.smul_{left,right}[_iff]` lemmas (#13003)