min_le_padicValRat_add — Mathlib

English

The minimum of the valuations of q and r is not greater than the valuation of q+r: min(v_p(q), v_p(r)) ≤ v_p(q+r).

Русский

Минимум v_p(q) и v_p(r) не превосходит v_p(q+r).

LaTeX

$$$ q,r \\neq 0 \\Rightarrow \\min\\{v_p(q), v_p(r)\\} \\le v_p(q+r) $$$

Lean4

/-- The minimum of the valuations of `q` and `r` is at most the valuation of `q + r`. -/
theorem min_le_padicValRat_add {q r : ℚ} (hqr : q + r ≠ 0) :
    min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r) :=
  (le_total (padicValRat p q) (padicValRat p r)).elim
    (fun h => by rw [min_eq_left h]; exact le_padicValRat_add_of_le hqr h)
    (fun h => by rw [min_eq_right h, add_comm]; exact le_padicValRat_add_of_le (by rwa [add_comm]) h)

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