∀ {R : Type u_2} {S : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : MulOneClass M]
  (f : S →+* R) (g : M →* R) (c : S) (φ : MonoidAlgebra S M),
  (MonoidAlgebra.liftNC ↑f ⇑g) (c • φ) = f c * (MonoidAlgebra.liftNC ↑f ⇑g) φ