radical_le_jacobson

Mathlib.RingTheory.Jacobson.Ideal

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

← MathLib Explorer

English

For a ring R, radical I is contained in Jac(I).

Русский

Для кольца R радикал I содержится в Jac(I).

LaTeX

$$$\operatorname{radical}(I) \le \operatorname{jacobson}(I)$$$

Lean4

theorem radical_le_jacobson : radical I ≤ jacobson I :=
  le_sInf fun _ hJ => (radical_eq_sInf I).symm ▸ sInf_le ⟨hJ.left, IsMaximal.isPrime hJ.right⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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