命題
A をネーター局所環とし、m をその極大イデアル、
M ≠ 0 を有限生成 A-加群とする。
k = A/m とおく。
極大な M-正則列の長さは正則列の取り方によらず一定である。
この長さは inf{p; Ext^p(k, M) ≠ 0} に等しい。

証明
>>34 から M-正則列の長さは dim(M) 以下である。
よって、>>29 より Ext^p(k, M) ≠ 0 となる 整数 p ≧ 0 が
存在する。よって、n = inf{p; Ext^(k, M) ≠ 0} とおけば、
n は有限である。>>29 と >>33 より極大な M-正則列の長さは
n である。
証明終