top_ne_set_smul_of_subset_jacobson_annihilator

English

If a set s is contained in the Jacobson annihilator, then the top submodule is not equal to s·top.

Русский

Если множество s лежит в Jacobson annihilator, то верхний подмодуль не равен s·верхний.

LaTeX

$$$$ \\top \\neq s \\cdot \\top, \\text{ if } s \\subseteq N.annihilator.jacobson. $$$$

Lean4

theorem top_ne_set_smul_of_subset_jacobson_annihilator [Nontrivial M] [Module.Finite R M] {s : Set R}
    (h : s ⊆ (Module.annihilator R M).jacobson) : (⊤ : Submodule R M) ≠ s • ⊤ :=
  ne_of_ne_of_eq (top_ne_ideal_smul_of_le_jacobson_annihilator (span_le.mpr h)) (span_smul_eq _ _)

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