instIsJacobsonRingOfIsArtinianRing

Mathlib.RingTheory.Jacobson.Ring

URI: https://scilib.ai/kg/mathlib#instIsJacobsonRingOfIsArtinianRing

English

If a ring R is Artinian, then R is a Jacobson ring.

Русский

Если кольцо R Артиненово конечного типа, то оно является кольцом Якобсона.

LaTeX

$$$[IsArtinianRing R] \\Rightarrow IsJacobsonRing R$.$$

Lean4

instance (priority := 100) [IsArtinianRing R] : IsJacobsonRing R :=
  isJacobsonRing_iff_prime_eq.mpr fun _ _ ↦ jacobson_eq_self_of_isMaximal

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

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

Разделы

Аффилиация

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