jacobson_eq_self_of_isMaximal

Mathlib.RingTheory.Jacobson.Ideal

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

English

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

Русский

Если I максимален, то Jac(I) = I.

LaTeX

$$$\text{If } I \text{ is maximal } \operatorname{jacobson}(I) = I$$$

Lean4

theorem jacobson_eq_self_of_isMaximal [H : IsMaximal I] : I.jacobson = I :=
  le_antisymm (sInf_le ⟨le_of_eq rfl, H⟩) le_jacobson

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

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

Разделы

Аффилиация

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