adicValued_apply

Mathlib.RingTheory.DedekindDomain.AdicValuation

URI: https://scilib.ai/kg/mathlib#IsDedekindDomain.HeightOneSpectrum.adicValued_apply

English

There exists a uniformizer π with valuation equal to -1, and the valuation map is surjective.

Русский

Существует униформизатор π с оценкой -1 и сюръективность оценки.

LaTeX

$$v.valuation_exists_uniformizer K$$

Lean4

theorem adicValued_apply {x : K} : v.adicValued.v x = v.valuation K x :=
  rfl

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

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

Разделы

Аффилиация

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