val_ne_zero

Mathlib.RingTheory.Valuation.Discrete.Basic

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

English

If π is a uniformizer, then π is not a unit and its value is positive.

Русский

Если π — uniformizer, то π не является единицей и его значение положительно.

LaTeX

$$v.IsUniformizer(π) ⇒ π ≠ 0 ∧ ¬IsUnit(π)$$

Lean4

theorem val_ne_zero (hπ : v.IsUniformizer π) : v π ≠ 0 :=
  by
  by_contra h0
  simp only [IsUniformizer, h0] at hπ
  exact (Units.ne_zero _).symm hπ

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

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

Разделы

Аффилиация

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