isRadical_of_eq_jacobson

Mathlib.RingTheory.Jacobson.Ideal

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

English

If Jac(I) = I, then I is radical.

Русский

Если Jac(I) = I, то I радикал.

LaTeX

$$$\operatorname{jacobson}(I) = I \Rightarrow I \text{ is radical}$$$

Lean4

theorem isRadical_of_eq_jacobson (h : jacobson I = I) : I.IsRadical :=
  radical_le_jacobson.trans h.le

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

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

Разделы

Аффилиация

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