toIocDiv — 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 `Ioc a (a + p)`. -/
def toIocDiv (a b : α) : ℤ :=
  (existsUnique_sub_zsmul_mem_Ioc hp b a).choose

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