eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator

English

Same as above: if N FG and N = r·N with r in Jacobson annihilator, then N = 0.

Русский

То же самое: если N FG и N = r·N, где r лежит в Jacobson annihilator, то N = 0.

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_pointwise_smul_of_mem_jacobson_annihilator {r : R} {N : Submodule R M} (hN : FG N)
    (hrN : N = r • N) (hrJac : r ∈ N.annihilator.jacobson) : N = ⊥ :=
  eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator hN (Eq.trans hrN (ideal_span_singleton_smul r N).symm)
    ((span_singleton_le_iff_mem r _).mpr hrJac)

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