of_ne_one_ne_zero — Mathlib

English

If p ≠ 1 and z ≠ 0, then padicValInt(p,z) equals the (p)‑adic multiplicity of z in integers.

Русский

Если p ≠ 1 и z ≠ 0, тогда padicValInt(p,z) равно p‑адической кратности z в целых числах.

LaTeX

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

Lean4

theorem of_ne_one_ne_zero {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) : padicValInt p z = multiplicity (p : ℤ) z :=
  by
  rw [padicValInt, padicValNat_def' hp (Int.natAbs_ne_zero.mpr hz)]
  apply Int.multiplicity_natAbs

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