{A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      {inst : CommRing A} →
        {inst_1 : Monoid G} →
          {inst_2 : AddCommMonoid W} → {inst_3 : Module A W} → {ρ : Representation A G W} → Subrepresentation ρ → ℕ