∀ (R : Type u_2) (M : Type u_1) [inst : Semiring R] [inst_1 : Add M] (x y : Multiplicative M),
  AddMonoidAlgebra.single (Multiplicative.toAdd (x * y)) 1 =
    AddMonoidAlgebra.single (Multiplicative.toAdd x) 1 * AddMonoidAlgebra.single (Multiplicative.toAdd y) 1