jacobson_top

Mathlib.RingTheory.Jacobson.Ideal

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

English

The Jacobson radical of the top ideal is the top ideal: Jac(⊤) = ⊤.

Русский

Радикал Якобиана верхнего идеала равен верхнему идеалу: Jac(⊤) = ⊤.

LaTeX

$$$\operatorname{jacobson}(\top) = \top$$$

Lean4

@[simp]
theorem jacobson_top : jacobson (⊤ : Ideal R) = ⊤ :=
  eq_top_iff.2 le_jacobson

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

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

Разделы

Аффилиация

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