isMaximal

Mathlib.RingTheory.Jacobson.Ideal

URI: https://scilib.ai/kg/mathlib#Ideal.jacobson.isMaximal

← MathLib Explorer

English

The Jacobson radical of a maximal ideal is maximal.

Русский

Радикал Якобиана максимального идеала также максимален.

LaTeX

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

Lean4

instance (priority := 100) isMaximal [H : IsMaximal I] : IsMaximal (jacobson I) :=
  ⟨⟨fun htop => H.1.1 (jacobson_eq_top_iff.1 htop), fun _ hJ => H.1.2 _ (lt_of_le_of_lt le_jacobson hJ)⟩⟩

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

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

Разделы

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

Аффилиация

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