eq_bot_of_set_smul_eq_of_subset_jacobson_annihilator

English

If N is finitely generated and N = s·N with s a set of elements contained in the Jacobson annihilator, then N = 0.

Русский

Если N FG и N = s·N для множества элементов s, лежащего в Jacobson annihilator, то N = 0.

LaTeX

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

Lean4

theorem eq_bot_of_set_smul_eq_of_subset_jacobson_annihilator {s : Set R} {N : Submodule R M} (hN : FG N)
    (hsN : N = s • N) (hsJac : s ⊆ N.annihilator.jacobson) : N = ⊥ :=
  eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator hN (Eq.trans hsN (span_smul_eq s N).symm) (span_le.mpr hsJac)

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