div' — Mathlib

English

If p is prime and m is coprime to p, then for any b with m | b, v_p(b/m) = v_p(b).

Русский

Если p — простое и gcd(p,m) = 1, тогда при любом b с m | b, v_p(b/m) = v_p(b).

LaTeX

$$$ m \\perp p \\Rightarrow m \\mid b \\Rightarrow v_p(b/m) = v_p(b) $$$

Lean4

protected theorem div' {m : ℕ} (cpm : Coprime p m) {b : ℕ} (dvd : m ∣ b) : padicValNat p (b / m) = padicValNat p b := by
  rw [padicValNat.div_of_dvd dvd, eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm), Nat.sub_zero]

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