val_le_one_iff

Mathlib.RingTheory.Valuation.Basic

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

English

There is a tight interplay between v(x) ≤ 1 and 1 ≤ v(x^{-1}) for nonzero x.

Русский

Существует тесная связь между v(x) ≤ 1 и 1 ≤ v(x^{-1}) для ненулевых x.

LaTeX

$$$ v(x) \\le 1 \\iff 1 \\le v(x^{-1}) $ (для x \\neq 0).$$

Lean4

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

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

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

Разделы

Аффилиация

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