padicValNat_eq_emultiplicity — Mathlib

English

For prime p and n ≠ 0, padicValNat(p,n) equals emultiplicity p n (as an ENat).

Русский

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

LaTeX

$$$\\\\mathrm{padicValNat}(p,n) = \\operatorname{emultiplicity}_p(n)$$$

Lean4

/-- A simplification of `padicValNat` when one input is prime, by analogy with
`padicValRat_def`. -/
theorem padicValNat_eq_emultiplicity [hp : Fact p.Prime] {n : ℕ} (hn : n ≠ 0) : padicValNat p n = emultiplicity p n :=
  by
  rw [(finiteMultiplicity_iff.2 ⟨hp.out.ne_one, Nat.pos_iff_ne_zero.mpr hn⟩).emultiplicity_eq_multiplicity]
  exact_mod_cast padicValNat_def hn

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