eq_bot_of_le_smul_of_le_jacobson_bot

English

Given suitable inclusions, the supremum with N and I•N' equals the supremum with N and J•N'.

Русский

При заданных условиях включения верхняя грань между N и I•N' равна верхней грани между N и J•N'.

LaTeX

$$$$ N' \\le N \\oplus I\\cdot N' \\implies N \\oplus N' = N \\oplus J\\cdot N'. $$$$

Lean4

/-- **Nakayama's Lemma** - Statement (2) in
[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).
See also `eq_smul_of_le_smul_of_le_jacobson` for a generalisation
to the `jacobson` of any ideal -/
@[stacks 00DV "(2)"]
theorem eq_bot_of_le_smul_of_le_jacobson_bot (I : Ideal R) (N : Submodule R M) (hN : N.FG) (hIN : N ≤ I • N)
    (hIjac : I ≤ jacobson ⊥) : N = ⊥ := by rw [eq_smul_of_le_smul_of_le_jacobson hN hIN hIjac, Submodule.bot_smul]

Похожие утверждения