instUniformSpace

Mathlib.RingTheory.LaurentSeries

URI: https://scilib.ai/kg/mathlib#LaurentSeries.instUniformSpace

English

The Laurent series ring K⟦X⟧ over a field K carries a natural uniform space structure.

Русский

Ринг Лорентцевых рядов K⟦X⟧ над полем K естественно снабжен равномерной структурой пространства.

LaTeX

$$$\\mathrm{UniformSpace}\\bigl(\\mathrm{LaurentSeries}\\,K\\bigr)$$$

Lean4

instance : UniformSpace K⸨X⸩ :=
  inferInstance

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

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

Разделы

Аффилиация

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