SMulCommClass of CommMonoid

Stream: Is there code for X?

[Andrew Yang]

Do we not have this?

import Mathlib.Algebra.Group.Action.Defs

instance {R M : Type*} [CommMonoid M] [SMul R M] [IsScalarTower R M M] : SMulCommClass R M M where
  smul_comm r s x := by
    rw [← one_smul M (s • x), ← smul_assoc, smul_comm, smul_assoc, one_smul]

[Kevin Buzzard]

    simp only [smul_eq_mul, mul_comm s, smul_mul_assoc]

avoids the 1. The s stops it looping :-)

[Junyan Xu]

apply? and rw? helped me find

import Mathlib.Algebra.Group.Action.Defs

instance {R M : Type*} [CommMonoid M] [SMul R M] [IsScalarTower R M M] :
    SMulCommClass R M M :=
  .of_mul_smul_one fun r m ↦ by rw [mul_comm, smul_one_mul]