isSemisimpleRing_iff_jacobson — Mathlib

English

Let R be a ring that is Artinian. Then R is semisimple if and only if its Jacobson radical is zero.

Русский

Пусть R — кольцо, удовлетворяющее условию Артиниана. Тогда R является полносемиструмным кольцом тогда и только тогда, когда его радикал Джейкобсона равен нулю.

LaTeX

$$$ \forall R\ [Ring\ R] [IsArtinianRing\ R],\ IsSemisimpleRing\ R \iff Ring.jacobson\ R = \bot $$$

Lean4

theorem isSemisimpleRing_iff_jacobson : IsSemisimpleRing R ↔ Ring.jacobson R = ⊥ :=
  IsArtinian.isSemisimpleModule_iff_jacobson R R

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