padicValNat_def — Mathlib

English

For prime p and n ≠ 0, padicValNat(p,n) equals multiplicity p n.

Русский

Для простого p и n ≠ 0, padicValNat(p,n) равно multiplicity p n.

LaTeX

$$$\\\\mathrm{padicValNat}(p,n) = \\\\operatorname{multiplicity}_p(n)$, \\\\text{при } p \\text{ prime и } n \\neq 0$$

Lean4

/-- A simplification of `padicValNat` when one input is prime, by analogy with
`padicValRat_def`. -/
theorem padicValNat_def [hp : Fact p.Prime] {n : ℕ} (hn : n ≠ 0) : padicValNat p n = multiplicity p n :=
  padicValNat_def' hp.out.ne_one hn

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