∀ {k : Type u_1} {G : Type u_2} {R : Type u_3} [inst : Semiring k] [inst_1 : AddMonoid G] [inst_2 : Semiring R]
  (f : k →+* R) (g : Multiplicative G →* R),
  (∀ (x : k) (y : Multiplicative G), Commute (f x) (g y)) →
    ∀ (_a _b : AddMonoidAlgebra k G),
      (AddMonoidAlgebra.liftNC ↑f ⇑g) (_a * _b) =
        (AddMonoidAlgebra.liftNC ↑f ⇑g) _a * (AddMonoidAlgebra.liftNC ↑f ⇑g) _b