English
modPart(p,r) is the integer representing the residue of r modulo p, given by r.num · gcdA(r.den,p) mod p.
Русский
modPart(p,r) — это целое число, представляющее остаток r по модулю p, заданное как r.num · gcdA(r.den,p) mod p.
LaTeX
$$\\operatorname{modPart}(p,r) = r.\\mathrm{num} \\cdot \\gcdA(r.\\mathrm{den},p) \\bmod p$$
Lean4
/-- `modPart p r` is an integer that satisfies
`‖(r - modPart p r : ℚ_[p])‖ < 1` when `‖(r : ℚ_[p])‖ ≤ 1`,
see `PadicInt.norm_sub_modPart`.
It is the unique non-negative integer that is `< p` with this property.
(Note that this definition assumes `r : ℚ`.
See `PadicInt.zmodRepr` for a version that takes values in `ℕ`
and works for arbitrary `x : ℤ_[p]`.) -/
def modPart : ℤ :=
r.num * gcdA r.den p % p
