instIsLocalRing

Mathlib.RingTheory.PowerSeries.Inverse

URI: https://scilib.ai/kg/mathlib#PowerSeries.instIsLocalRing

English

If R is a local ring, then the ring of formal power series R⟦X⟧ is also a local ring.

Русский

Если R локальная кольцо, то кольцо формальных степенных рядов R⟦X⟧ также локальное.

LaTeX

$$$ IsLocalRing(R[[X]]) \text{ given } IsLocalRing(R). $$$

Lean4

instance : IsLocalRing R⟦X⟧ :=
  { inferInstanceAs <| IsLocalRing <| MvPowerSeries Unit R with }

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

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

Разделы

Аффилиация

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