instValuationRingInteger

Mathlib.RingTheory.Valuation.ValuationRing

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

English

For a valuation v on a field K, the subring v.integer is itself a valuation ring.

Русский

Для валиации v на поле K подкольцо v.integer само является валюационным кольцом.

LaTeX

$$$\text{ValuationRing}(v.\operatorname{integer})$$$

Lean4

instance instValuationRingInteger (v : Valuation K Γ) : ValuationRing v.integer :=
  of_integers (v := v) (Valuation.integer.integers v)

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

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

Разделы

Аффилиация

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