padicValNat_def' — Mathlib

English

If p ≠ 1 and n ≠ 0, then padicValNat(p,n) equals multiplicity p n.

Русский

Если p ≠ 1 и n ≠ 0, то padicValNat(p,n) равно multiplicity p n.

LaTeX

$$$\\\\mathrm{padicValNat}(p,n) = \\operatorname{multiplicity}_p(n) \\\\text{обусловлено } (p \\neq 1) \\land (n \\neq 0)$$$

Lean4

theorem padicValNat_def' {n : ℕ} (hp : p ≠ 1) (hn : n ≠ 0) : padicValNat p n = multiplicity p n :=
  by
  simp only [padicValNat, ne_eq, hp, not_false_eq_true, Nat.pos_iff_ne_zero.mpr hn, and_self, ↓reduceDIte, multiplicity,
    emultiplicity, finiteMultiplicity_iff.mpr ⟨hp, Nat.pos_iff_ne_zero.mpr hn⟩]
  convert (WithTop.untopD_coe ..).symm

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