∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Semiring R] [inst_1 : SMulZeroClass N R]
  [inst_2 : SMulZeroClass O R] [SMulCommClass N O R], SMulCommClass N O (AddMonoidAlgebra R M)