integer

Mathlib.Topology.Algebra.Valued.ValuedField

URI: https://scilib.ai/kg/mathlib#Valued.integer

← MathLib Explorer

English

The valuation ring 𝒪[K] of a valued field K is a subring of K.

Русский

Ценностное кольцо 𝒪[K] valued-поля K является подкольцом K.

LaTeX

$$$\\mathcal{O}_K \\le K \\quad\\text{is a subring}$$$

Lean4

/-- A `Valued` version of `Valuation.integer`, enabling the notation `𝒪[K]` for the
valuation integers of a valued field `K`. -/
@[reducible]
def integer : Subring K :=
  (vK.v).integer

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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