Length bound for a Schur module (source code)

= Length bound for a Schur module
{title2=$D_\lambda(\mathbb C^m)\ne0\iff\ell(\lambda)\le m$}

A column of length greater than $m$ antisymmetrizes more than $m$ vectors, giving zero. When there are at most $m$ rows, place the $i$th <basis> vector in every tensor position of row $i$. Row symmetrization multiplies by a nonzero factorial product, and column antisymmetrization is nonzero because the vectors in every column are distinct. This proves the precise nonvanishing criterion for a <Schur module>.