jacobson_le_annihilator — Mathlib

English

If R is a semisimple ring, then its Jacobson radical is zero (via the module formulation).

Русский

Если R — полупростое кольцо, то радикал Якобсона равен нулю.

LaTeX

$$Ring.jacobson R = ⊥$$

Lean4

/-- The Jacobson radical of a ring annihilates every semisimple module. -/
theorem jacobson_le_annihilator [IsSemisimpleModule R M] : Ring.jacobson R ≤ Module.annihilator R M := fun r hr ↦
  Module.mem_annihilator.mpr fun m ↦
    by
    have := Module.le_comap_jacobson (LinearMap.toSpanSingleton R M m) hr
    rwa [jacobson_eq_bot] at this

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