le_of_le_smul_of_le_jacobson_bot — Mathlib

English

If N' is FG and I ≤ jacobson ⊥, and N' ≤ N ⊔ I•N', then N' ≤ N.

Русский

Если N' FG, I ≤ jacobson ⊥ и N' ≤ N ⊔ I•N', то N' ≤ N.

LaTeX

$$$$ \\text{If } N' \\text{ is FG and } I \\le \\operatorname{jacobson}(\\bot) \\\\text{and } N' \\le N \\oplus I\\cdot N', \\text{ then } N' \\le N. $$$$

Lean4

theorem le_of_le_smul_of_le_jacobson_bot {R M} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R}
    {N N' : Submodule R M} (hN' : N'.FG) (hIJ : I ≤ jacobson ⊥) (hNN : N' ≤ N ⊔ I • N') : N' ≤ N := by
  rw [← sup_eq_left, sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul, sup_bot_eq]

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