jacobson_lt_top — Mathlib

English

For a nontrivial module M over a ring R, the Jacobson radical is strictly below the top submodule.

Русский

Для не тривиального модуля M над кольцом R радикал Якобсона строго меньше верхнего подмодуля.

LaTeX

$$jacobson R M < ⊤$$

Lean4

theorem jacobson_lt_top [Nontrivial M] [IsCoatomic (Submodule R M)] : jacobson R M < ⊤ :=
  by
  obtain ⟨m, hm, -⟩ := (eq_top_or_exists_le_coatom (⊥ : Submodule R M)).resolve_left bot_ne_top
  exact (sInf_le <| Set.mem_setOf.mpr hm).trans_lt hm.1.lt_top

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