instIsJacobsonRingOfKrullDimLEOfNatNat

Mathlib.RingTheory.KrullDimension.Zero

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

English

If Ring.KrullDimLE 0 R, then R is a Jacobson ring.

Русский

Если кольцо R удовлетворяет Ring.KrullDimLE 0, то R является кольцом Якобсона.

LaTeX

$$[Ring.KrullDimLE 0 R] ⇒ IsJacobsonRing R$$

Lean4

instance (priority := 100) [Ring.KrullDimLE 0 R] : IsJacobsonRing R :=
  ⟨fun I hI ↦ by rw [I.jacobson_eq_radical, hI.radical]⟩

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

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

Разделы

Аффилиация

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