toIocMod_eq_sub_fract_mul — Mathlib

English

Analogously, the IocMod value from a to b equals a plus p minus the fractional part times p.

Русский

Аналогично: IocMod hp a b = a + p − fract((a + p − b)/p) · p.

LaTeX

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

Lean4

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

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