toIocMod — Mathlib

English

toIocMod hp a b is defined as b minus the appropriate multiple of p, yielding the representative of b in the interval (a, a+p].

Русский

toIocMod hp a b задаётся как b минус соответствующее кратное p, являющее представителем b в интервале (a, a+p].

LaTeX

$$$ \mathrm{toIocMod}(hp,a,b) = b - \mathrm{toIocDiv}(hp,a,b) \cdot p $$$

Lean4

/-- Reduce `b` to the interval `Ioc a (a + p)`. -/
def toIocMod (a b : α) : α :=
  b - toIocDiv hp a b • p

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