∀ {A : Type u_2} {G : Type u_3} {W : Type u_1} [inst : CommRing A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} (N : Submodule (MonoidAlgebra A G) ρ.asModule) (a : A),
  ∀ w ∈ N.carrier, a • w ∈ N.carrier