Multiplicity bounds the length of a holonomic Weyl module (source code)

= Multiplicity bounds the length of a holonomic Weyl module
{title2=$\operatorname{length}(M)\leq m(M)$}

Every nonzero subquotient of a <holonomic Weyl algebra module> over a characteristic-zero <field> has dimension $n$, by <Bernstein inequality for Weyl algebra modules> and <dimension and multiplicity in a filtered exact sequence>. Each strict step in a <submodule> chain consumes positive <multiplicity of a filtered module>. With a <standard graded algebra> normalization these multiplicities are integral. There are therefore at most $m(M)$ strict steps. The <module> is <Artinian> and <Noetherian>, and its <module length> is bounded by that multiplicity.