instIsJacobsonRing

Mathlib.RingTheory.Jacobson.Ring

URI: https://scilib.ai/kg/mathlib#Polynomial.instIsJacobsonRing

English

If R is Jacobson, then the instance states IsJacobsonRing R[X].

Русский

Если R — кольцо Якобсона, то инстанс утверждает, что R[X] также Якобсон.

LaTeX

$$$IsJacobsonRing(R[X])$$$

Lean4

instance [IsJacobsonRing R] : IsJacobsonRing R[X] :=
  isJacobsonRing_polynomial_iff_isJacobsonRing.mpr ‹IsJacobsonRing R›

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

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

Разделы

Аффилиация

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