jacobson_lt_top

Mathlib.RingTheory.Jacobson.Radical

URI: https://scilib.ai/kg/mathlib#Ring.jacobson_lt_top

English

For a nontrivial ring R, the Jacobson radical is strictly smaller than the top submodule.

Русский

Для ненулевого кольца R радикал Якобсона строго меньше верхнего подмодуля.

LaTeX

$$$\\text{If } \\; R \\text{ is nontrivial, then } \\operatorname{jacobson}(R) < \\top.$$$

Lean4

theorem jacobson_lt_top [Nontrivial R] : jacobson R < ⊤ :=
  Module.jacobson_lt_top R R

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

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

Разделы

Аффилиация

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