jacobson_eq_bot_of_injective — Mathlib

English

For a nontrivial module M, the Jacobson radical of M is strictly below the top submodule.

Русский

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

LaTeX

$$jacobson R M < ⊤$$

Lean4

theorem jacobson_eq_bot_of_injective (inj : Function.Injective f) (h : jacobson R₂ M₂ = ⊥) : jacobson R M = ⊥ :=
  le_bot_iff.mp <| (le_comap_jacobson f).trans <| by simp_rw [h, comap_bot, ((LinearMapClass.ker_eq_bot _).mpr inj).le]

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