top_ne_pointwise_smul_of_mem_jacobson_annihilator

English

If r lies in the Jacobson annihilator, then the top submodule is not equal to r-times the top.

Русский

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

LaTeX

$$$$ \\top \\neq \\; r \\cdot \\top, \\text{ with } r \\in (\\operatorname{annihilator} R M).jacobson. $$$$

Lean4

theorem top_ne_pointwise_smul_of_mem_jacobson_annihilator [Nontrivial M] [Module.Finite R M] {r}
    (h : r ∈ (Module.annihilator R M).jacobson) : (⊤ : Submodule R M) ≠ r • ⊤ :=
  ne_of_ne_of_eq (top_ne_set_smul_of_subset_jacobson_annihilator <| Set.singleton_subset_iff.mpr h)
    (singleton_set_smul ⊤ r)

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