eq_bot_of_le_jacobson_smul — Mathlib

English

For an FG submodule N of a module M over a ring R, if N ≠ ⊥ then Jac(R) • N < N.

Русский

Для FG-подмодуля N модуля M над R, если N ≠ 0, то Jac(R) • N < N.

LaTeX

$$$N \\neq \\bot \\;\\Rightarrow\\; \\operatorname{jacobson}(R) \\cdot N < N.$$$

Lean4

/-- A form of Nakayama's lemma for modules over noncommutative rings. -/
theorem eq_bot_of_le_jacobson_smul {N : Submodule R M} (fg : N.FG) (le : N ≤ Ring.jacobson R • N) : N = ⊥ := by
  contrapose! le; exact (jacobson_smul_lt le fg).not_ge

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