jacobson_eq_radical

Mathlib.RingTheory.KrullDimension.Zero

URI: https://scilib.ai/kg/mathlib#Ideal.jacobson_eq_radical

English

For any ideal I in a ring with KrullDimLE 0, the Jacobson radical of I equals the radical of I.

Русский

Для любого идеала I в кольце с KrullDimLE 0 радикал Якобсона I равен радикалу I.

LaTeX

$$$I^{\\mathrm{jacobson}} = I^{\\radical}$$$

Lean4

theorem jacobson_eq_radical [Ring.KrullDimLE 0 R] : I.jacobson = I.radical := by
  simp [jacobson, radical_eq_sInf, Ideal.isMaximal_iff_isPrime]

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

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

Разделы

Аффилиация

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