one_le_val_iff

Mathlib.RingTheory.Valuation.Basic

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

English

For x ≠ 0, 1 ≤ v(x) iff 1 ≤ v(x^{-1}).

Русский

Для x ≠ 0: 1 ≤ v(x) эквивалентно 1 ≤ v(x^{-1}).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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