one_lt_val_iff

Mathlib.RingTheory.Valuation.Basic

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

English

For a valuation v on a division ring K and nonzero x, 1 < v(x) iff v(x^{-1}) < 1.

Русский

Для валидации v на поля x ≠ 0: 1 < v(x) тогда и только тогда, когда v(x^{-1}) < 1.

LaTeX

$$$ 1 < v(x) \\iff v(x^{-1}) < 1 \\quad (x \\neq 0) $$$

Lean4

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

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

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

Разделы

Аффилиация

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