instIsDiscreteValuationRing

Mathlib.RingTheory.PowerSeries.Inverse

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

English

Let k be a field. The ring of formal power series k[[X]] is a discrete valuation ring.

Русский

Пусть k — поле. Кольцо формальных степенных рядов k[[X]] является дискретным ценностным кольцом.

LaTeX

$$$k\![[X]]$ is a discrete valuation ring.$$

Lean4

instance : IsDiscreteValuationRing k⟦X⟧ :=
  ofHasUnitMulPowIrreducibleFactorization hasUnitMulPowIrreducibleFactorization

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

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

Разделы

Аффилиация

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