of_int_multiplicity — Mathlib

English

If p ≠ 1 and z ≠ 0, the p-adic value of z (as a rational) equals the multiplicity of p in z.

Русский

Если p ≠ 1 и z ≠ 0, p‑адическая оценка z в рациональном числе равна кратности p в z.

LaTeX

$$$\mathrm{padicValRat}(p,z) = \operatorname{multiplicity}(p:\mathbb{Z})\,z$ при $p\neq 1$, $z\neq 0$$$

Lean4

/-- The `p`-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`. -/
theorem of_int_multiplicity {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) : padicValRat p (z : ℚ) = multiplicity (p : ℤ) z := by
  rw [of_int, padicValInt.of_ne_one_ne_zero hp hz]

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