toIcoMod_eq_add_fract_mul — Mathlib

English

The IcoMod value can be expressed as a shift by a plus a fractional part times p, i.e., the fractional part of (b − a)/p scaled by p added to a.

Русский

Значение IcoMod выражается как сдвиг на a плюс дробная часть (b − a)/p, умноженная на p.

LaTeX

$$$$ \operatorname{toIcoMod}(hp, a, b) = a + \operatorname{fract}\left(\frac{b - a}{p}\right) \cdot p $$$$

Lean4

theorem toIcoMod_eq_add_fract_mul (a b : α) : toIcoMod hp a b = a + Int.fract ((b - a) / p) * p :=
  by
  rw [toIcoMod, toIcoDiv_eq_floor, Int.fract]
  simp [field, -Int.self_sub_floor]
  ring

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