val_lt_one

Mathlib.RingTheory.Valuation.Discrete.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.IsUniformizer.val_lt_one

English

Alternative expression: for a uniformizer π, v(π) equals the generator of value group.

Русский

Альтернативно: для uniformizer π выполняется v(π) = генератор группы значений.

LaTeX

$$v(π) = generator(v)$$

Lean4

theorem val_lt_one (hπ : v.IsUniformizer π) : v π < 1 :=
  hπ ▸ hv.generator_lt_one

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

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

Разделы

Аффилиация

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