∀ (A : Type u_1) (M : Type u_2) [inst : Semiring A] [inst_1 : AddMonoid M] (x y : AddMonoidAlgebra A M),
  (AddMonoidAlgebra.toMultiplicative A M).toFun (x * y) =
    (AddMonoidAlgebra.toMultiplicative A M).toFun x * (AddMonoidAlgebra.toMultiplicative A M).toFun y