isRadical_jacobson

Mathlib.RingTheory.Jacobson.Ideal

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

English

The Jacobson radical of I is radical.

Русский

Радикал Якобиана I является радикалом.

LaTeX

$$$\operatorname{isRadical}(\operatorname{jacobson}(I))$$$

Lean4

theorem isRadical_jacobson (I : Ideal R) : I.jacobson.IsRadical :=
  isRadical_of_eq_jacobson jacobson_idem

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

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

Разделы

Аффилиация

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