toIcoDiv — Mathlib

English

There exists a unique integer n such that b − n·p lies in the half-open interval [a, a + p).

Русский

Существует единственный целый число n так, что b − n·p принадлежит полуинтервалу [a, a + p).

LaTeX

$$$\exists! n \in \mathbb{Z},\; b - n p \in [a, a + p)$$$

Lean4

/-- The unique integer such that this multiple of `p`, subtracted from `b`, is in `Ico a (a + p)`. -/
def toIcoDiv (a b : α) : ℤ :=
  (existsUnique_sub_zsmul_mem_Ico hp b a).choose

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