MulAction Nat on AddMonoid

Stream: Is there code for X?

[Yakov Pechersky]

I couldn't find this when I was trying to use smul_comm on nsmuls:

import Mathlib.Algebra.GroupPower.Basic
import Mathlib.Data.Nat.Basic
import Mathlib.GroupTheory.GroupAction.Defs

variable {M : Type*} [AddMonoid M]

instance : MulAction ℕ M := by infer_instance -- we don't have this?

instance : MulAction ℕ M where
  smul r x := r • x
  one_smul := one_nsmul
  mul_smul _ _ _ := mul_nsmul' _ _ _

[Eric Wieser]

Are you missing an import? (edit: no)

[Eric Wieser]

Maybe we only have this when M is commutative

[Yakov Pechersky]

Thanks. In the file I was working in, it has very basic imports so no Modules. Makes sense.