submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul

Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV

submodule.fg_of_fg_map_of_fg_inf_ker

If 0 → M' → M → M'' → 0 is exact and M' and M'' are finitely generated then so is M.