padicValRat — Mathlib

English

The p-adic valuation of a rational q is the p-adic valuation of its numerator minus the p-adic valuation of its denominator.

Русский

p‑адическая оценка рационального числа q равна разности p‑адикальных оценок его числителя и знаменателя.

LaTeX

$$$\mathrm{padicValRat}(p,q) = \mathrm{padicValInt}(p,q.num) - \mathrm{padicValNat}(p,q.den)$$$

Lean4

/-- `padicValRat` defines the valuation of a rational `q` to be the valuation of `q.num` minus the
valuation of `q.den`. If `q = 0` or `p = 1`, then `padicValRat p q` defaults to `0`. -/
def padicValRat (p : ℕ) (q : ℚ) : ℤ :=
  padicValInt p q.num - padicValNat p q.den

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