val_pos

Mathlib.RingTheory.Valuation.Discrete.Basic

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

English

If π is a uniformizer then v(π) > 0.

Русский

Если π — uniformizer, то v(π) > 0.

LaTeX

$$v(π) > 0$$

Lean4

theorem val_pos (hπ : IsUniformizer v π) : 0 < v π := by rw [IsUniformizer.iff] at hπ; simp [zero_lt_iff, ne_eq, hπ]

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

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

Разделы

Аффилиация

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