padicValNat_eq_maxPowDiv — Mathlib

English

For any prime p and natural numbers n, the p-adic valuation of n equals the largest exponent k such that p^k divides n.

Русский

Для любых p и n ∈ Nat p‑адическая оценка числа n равна наибольшему показателю k, для которого p^k делит n.

LaTeX

$$$\mathrm{padicValNat}(p,n) = \mathrm{maxPowDiv}(p,n)$$$

Lean4

/-- Allows for more efficient code for `padicValNat` -/
@[csimp]
theorem padicValNat_eq_maxPowDiv : @padicValNat = @maxPowDiv :=
  by
  ext p n
  by_cases h : 1 < p ∧ 0 < n
  · rw [padicValNat_def' h.1.ne' h.2.ne', maxPowDiv_eq_multiplicity h.1 h.2.ne']
    exact Nat.finiteMultiplicity_iff.2 ⟨h.1.ne', h.2⟩
  · simp only [not_and_or, not_gt_eq, Nat.le_zero] at h
    apply h.elim
    · intro h
      interval_cases p
      · simp [Classical.em]
      · dsimp [padicValNat, maxPowDiv]
        rw [go, if_neg]; simp
    · intro h
      simp [h]

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