jacobson_smul_top_le — Mathlib

English

The product of Jacobson radical with the top submodule is contained in the Jacobson radical of the module: Jac(R) • ⊤ ≤ Module.jacobson R M.

Русский

Произведение радикала Якобсона и верхнего подмодуля вложено в радикал Якобсона модуля: jacobson(R) • ⊤ ≤ Module.jacobson R M.

LaTeX

$$$\\operatorname{jacobson}(R) \\cdot \\top \\le \\operatorname{Module.jacobson}(R, M).$$$

Lean4

theorem jacobson_smul_top_le : jacobson R • (⊤ : Submodule R M) ≤ Module.jacobson R M :=
  Submodule.smul_le.mpr fun _ hr m _ ↦ Module.le_comap_jacobson (LinearMap.toSpanSingleton R M m) hr

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