of_nat — Mathlib

English

The p-adic valuation of a natural number n as a rational agrees with its natural valuation (when cast appropriately).

Русский

p‑адикальная оценка натурального числа n как рационала совпадает с его натуральной оценкой.

LaTeX

$$$\mathrm{padicValNat}(p,n)\;\text{cast} = \mathrm{padicValRat}(p,n.cast)$$$

Lean4

/-- The `p`-adic value of an integer `z ≠ 0` is its `p`-adic value as a rational. -/
@[simp]
theorem of_nat {n : ℕ} : padicValRat p n = padicValNat p n := by simp [padicValRat]

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