val_le_one_or_val_inv_lt_one — Mathlib

English

A weaker symmetric form: val_le_one_or_val_inv_lt_one holds, i.e., v(x) ≤ 1 or v(x^{-1}) < 1.

Русский

Слабая симметричная форма: либо v(x) ≤ 1, либо v(x^{-1}) < 1.

LaTeX

$$$ v(x) \\le 1 \\lor v(x^{-1}) < 1 $$$

Lean4

theorem val_le_one_or_val_inv_lt_one (v : Valuation K Γ₀) (x : K) : v x ≤ 1 ∨ v x⁻¹ < 1 :=
  by
  by_cases h : x = 0
  · simp only [h, map_zero, zero_le', inv_zero, zero_lt_one, or_self]
  · simp only [← one_lt_val_iff v h, le_or_gt]

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