add_eq_of_lt — Mathlib

English

If q,r ≠ 0 and v_p(q) < v_p(r), then v_p(q+r) = v_p(q) (provided nonzero sum).

Русский

Если q,r ≠ 0 и v_p(q) < v_p(r), то v_p(q+r) = v_p(q) (при условии ненулности суммы).

LaTeX

$$$ q,r \\neq 0 \\Rightarrow v_p(q) < v_p(r) \\Rightarrow v_p(q+r) = v_p(q) $$$

Lean4

theorem add_eq_of_lt {q r : ℚ} (hqr : q + r ≠ 0) (hq : q ≠ 0) (hr : r ≠ 0) (hval : padicValRat p q < padicValRat p r) :
    padicValRat p (q + r) = padicValRat p q := by rw [add_eq_min hqr hq hr (ne_of_lt hval), min_eq_left (le_of_lt hval)]

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