конечнопорождённость и нётеровость

[beroal]

В учебнике по алгебраической теории чисел есть ссылка на следующую теорему.

Цитата:

Подгруппа конечнопорождённой абелевой группы конечнопорождённа.

Я так понимаю, это частный случай следующей теоремы, считая абелевы группы $\mathbb{Z}$-модулями.

Цитата:

Если $R$ — правое нётерово кольцо и $M$ — конечнопорождённый правый $R$-модуль, тогда любой правый подмодуль $M$ конечнопорождён.

Доказательство этой теоремы в учебнике по абстрактной алгебре Ernest Shult и David Surowski плотно используёт нётеровость. Я правильно понимаю, что это доказательство неконструктивно, то есть, хотя порождающее множество конечно, доказательство не содержит способа его вычислить? По крайней мере, я не представляю, как вычислять исходя из нётеровости. А есть конструктивное?