val_lt_one_iff

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.val_lt_one_iff

English

v(x) = 1 iff v(x^{-1}) = 1 for a valuation on a division ring K.

Русский

v(x) = 1 тогда и только тогда, когда v(x^{-1}) = 1.

LaTeX

$$$ v(x) = 1 \\iff v(x^{-1}) = 1 $$$

Lean4

theorem val_lt_one_iff (v : Valuation K Γ₀) {x : K} (h : x ≠ 0) : v x < 1 ↔ 1 < v x⁻¹ := by
  simp [one_lt_inv₀ (v.pos_iff.2 h)]

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

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

Разделы

Аффилиация

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