∀ {ι : Type u_1} (A : ι → Type u_2) [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] {i : ι} (a : A i) (n : ℕ),
  GradedMonoid.mk i a ^ n = GradedMonoid.mk (n • i) (GradedMonoid.GMonoid.gnpow n a)