div — Mathlib

English

Dividing out by a prime factor decreases the p-adic valuation by exactly 1: if p ∣ b, then v_p(b/p) = v_p(b) − 1.

Русский

Разделение на простое p уменьшает p-адикальную величину на единицу: если p делит b, то v_p(b/p) = v_p(b) − 1.

LaTeX

$$$ p \\mid b \\Rightarrow v_p(b/p) = v_p(b) - 1 $$$

Lean4

/-- Dividing out by a prime factor reduces the `padicValNat` by `1`. -/
protected theorem div (dvd : p ∣ b) : padicValNat p (b / p) = padicValNat p b - 1 := by
  rw [padicValNat.div_of_dvd dvd, padicValNat_self]

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