toIcoMod — Mathlib

English

toIcoMod hp a b is defined as b minus the appropriate multiple of p, yielding the representative of b in the interval [a, a+p).

Русский

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

LaTeX

$$$ \mathrm{toIcoMod}(hp,a,b) = b - \mathrm{toIcoDiv}(hp,a,b) \cdot p $$$

Lean4

/-- Reduce `b` to the interval `Ico a (a + p)`. -/
def toIcoMod (a b : α) : α :=
  b - toIcoDiv hp a b • p

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