∀ {ι : Type u_1} {R : Type u_3} {A : Type u_2} [inst : AddMonoid ι] [inst_1 : CommSemiring R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (x : R) (x_1 : GradedMonoid fun x => A),
  GradedMonoid.mk 0 ((algebraMap R A).toAddMonoidHom x) * x_1 =
    x_1 * GradedMonoid.mk 0 ((algebraMap R A).toAddMonoidHom x)