∀ {G : Type u_2} {M : Type u_6} {α : Type u_7} [inst : Monoid G] [inst_1 : AddCommMonoid M] [inst_2 : MulAction G α]
  (g : G) (f : SkewMonoidAlgebra M α), g • f = (SkewMonoidAlgebra.mapDomain fun x => g • x) f