div — Mathlib

English

If q,r ≠ 0 are rationals, then v_p(q/r) = v_p(q) − v_p(r).

Русский

Если q,r ≠ 0 — рациональные числа, то v_p(q/r) = v_p(q) − v_p(r).

LaTeX

$$$ q \\neq 0 \\land r \\neq 0 \\Rightarrow v_p\\left(\\dfrac{q}{r}\\right) = v_p(q) - v_p(r) $$$

Lean4

/-- A rewrite lemma for `padicValRat p (q / r)` with conditions `q ≠ 0`, `r ≠ 0`. -/
protected theorem div {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) : padicValRat p (q / r) = padicValRat p q - padicValRat p r :=
  by rw [div_eq_mul_inv, padicValRat.mul hq (inv_ne_zero hr), padicValRat.inv r, sub_eq_add_neg]

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