isJacobsonRing_iff

Mathlib.RingTheory.Jacobson.Ring

URI: https://scilib.ai/kg/mathlib#isJacobsonRing_iff

English

If a ring R is Artinian, then R is a Jacobson ring.

Русский

Если кольцо R конечно по длине (артиново), то оно является кольцом Якобсона.

LaTeX

$$$\\text{If } R \\text{ is Artinian, then } R \\text{ is Jacobson.}$$$

Lean4

theorem isJacobsonRing_iff {R} [CommRing R] : IsJacobsonRing R ↔ ∀ I : Ideal R, I.IsRadical → I.jacobson = I :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru