of_field

Mathlib.RingTheory.Valuation.ValuationRing

URI: https://scilib.ai/kg/mathlib#ValuationRing.of_field

English

Every field K is a valuation ring of itself (with the trivial valuation).

Русский

Каждое поле K является валюационным кольцом над самим собой (с тривиальной валюацией).

LaTeX

$$$K \text{ is a valuation ring of } K$$$

Lean4

/-- A field is a valuation ring. -/
instance (priority := 100) of_field : ValuationRing K :=
  inferInstance

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

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

Разделы

Аффилиация

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