eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator

English

If a finitely generated submodule N satisfies N = r·N for some element r in the Jacobson annihilator, then N = 0.

Русский

Если FG-подмодуль N удовлетворяет N = r·N для некоторого r из Jacobi-аннигилизатора, то N нулевой.

LaTeX

$$$$ \\text{If } N \\text{ is FG and } N = r \\cdot N, \\ r \\in N.annihilator.jacobson, \\text{ then } N = 0. $$$$

Lean4

theorem eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator {I : Ideal R} {N : Submodule R M} (hN : FG N)
    (hIN : N = I • N) (hIjac : I ≤ N.annihilator.jacobson) : N = ⊥ :=
  (eq_smul_of_le_smul_of_le_jacobson hN hIN.le hIjac).trans N.annihilator_smul

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