∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {V : Type u_3} [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V]
  (W : Submodule k V),
  (∀ (g : G), ∀ v ∈ W, (MonoidAlgebra.of k G) g • v ∈ W) → ∀ (c : MonoidAlgebra k G) {x : V}, x ∈ ↑W → c • x ∈ ↑W