Holonomic Weyl algebra module (source code)

= Holonomic Weyl algebra module
{title2=$d(M)=n$}

A nonzero finitely generated <Weyl algebra> module over $A_n(\mathbb C)$ is holonomic when it attains the lower bound in the <Bernstein inequality for Weyl algebra modules>. The zero module is also conventionally called holonomic. Nonzero subquotients of a holonomic module remain holonomic. Additivity and integrality of the leading Hilbert-polynomial multiplicity then bound the number of nonzero factors in any submodule chain, giving finite composition length.