val_le_one_or_val_inv_le_one — Mathlib

English

A symmetric variant: v(x) ≤ 1 or v(x)^{-1} ≤ 1.

Русский

Симметричный вариант: v(x) ≤ 1 или v(x)^{-1} ≤ 1.

LaTeX

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

Lean4

/-- This theorem is a weaker version of `Valuation.val_le_one_or_val_inv_lt_one`, but more symmetric
in `x` and `x⁻¹`.
-/
theorem val_le_one_or_val_inv_le_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, or_self]
  · simp only [← one_le_val_iff v h, le_total]

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