English
Let I be an ideal of R and N, N' ⊆ M be submodules with N'.FG. If I ⊆ jacobson(0) and N' ≤ N ⊔ I·N', then I·N' ≤ N.
Русский
Пусть I — идеал кольца R, N, N' — подмодули модуля M, причём N' порождён конечнопорожденной частью. Если I ⊆ jacobson(0) и N' ⊆ N ⊔ (I·N'), то I·N' ⊆ N.
LaTeX
$$$ N'.FG \\land I \\le \\operatorname{jacobson}(\\{0\\}) \\land N' \\le N \\sqcup I \\cdot N' \\Rightarrow I \\cdot N' \\le N $$$
Lean4
/-- **Nakayama's Lemma** - Statement (4) in
[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).
See also `sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson` for a generalisation
to the `jacobson` of any ideal -/
@[stacks 00DV "(4)"]
theorem smul_le_of_le_smul_of_le_jacobson_bot {I : Ideal R} {N N' : Submodule R M} (hN' : N'.FG) (hIJ : I ≤ jacobson ⊥)
(hNN : N' ≤ N ⊔ I • N') : I • N' ≤ N :=
smul_le_right.trans (le_of_le_smul_of_le_jacobson_bot hN' hIJ hNN)
