jacobson_le_ker — Mathlib

English

If M₂ is a semisimple module, then the Jacobson radical of R acting on M is contained in the kernel of a morphism f: M → M₂.

Русский

Если M₂ — полупростый модуль, то радикал Якобсона модуля M лежит в ядре отображения f: M → M₂.

LaTeX

$$Module.jacobson R M ≤ LinearMap.ker f$$

Lean4

theorem jacobson_le_ker [IsSemisimpleModule R₂ M₂] : Module.jacobson R M ≤ LinearMap.ker f :=
  (Module.le_comap_jacobson f).trans <| by simp_rw [jacobson_eq_bot, LinearMap.ker, le_rfl]

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