padicValRat_def — Mathlib

English

PadicValRat is defined by the difference of padicValInt of the numerator and padicValNat of the denominator.

Русский

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

LaTeX

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

Lean4

theorem padicValRat_def (p : ℕ) (q : ℚ) : padicValRat p q = padicValInt p q.num - padicValNat p q.den :=
  rfl

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