∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k]
  {f g : SkewMonoidAlgebra k G →+* k},
  f = g ↔
    f.comp SkewMonoidAlgebra.singleOneRingHom = g.comp SkewMonoidAlgebra.singleOneRingHom ∧
      (↑f).comp (SkewMonoidAlgebra.of k G) = (↑g).comp (SkewMonoidAlgebra.of k G)