∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} {f : G → G'} {a : G} {b : k},
  (SkewMonoidAlgebra.mapDomain f) (SkewMonoidAlgebra.single a b) = SkewMonoidAlgebra.single (f a) b