div_of_dvd — Mathlib

English

For p-adic valuation, v_p(q/d) = v_p(q) − v_p(d) whenever d ≠ 0 and q ≠ 0 and d divides q in the sense of rationals.

Русский

Для p-адикальной величины при делении q/d верно: v_p(q/d) = v_p(q) − v_p(d), когда d ≠ 0 и q ≠ 0.

LaTeX

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

Lean4

protected theorem div_of_dvd (h : b ∣ a) : padicValNat p (a / b) = padicValNat p a - padicValNat p b :=
  by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp
  obtain ⟨k, rfl⟩ := h
  obtain ⟨hb, hk⟩ := mul_ne_zero_iff.mp ha
  rw [mul_comm, k.mul_div_cancel hb.bot_lt, padicValNat.mul hk hb, Nat.add_sub_cancel]

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