toIcoMod_eq_fract_mul — Mathlib

English

In the zero-to-b basis, the IcoMod value for the second argument is the fractional part of the scaled value times p.

Русский

В базисе ноль до b значение IcoMod равно дробной части умноженной на p.

LaTeX

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

Lean4

theorem toIcoMod_eq_fract_mul (b : α) : toIcoMod hp 0 b = Int.fract (b / p) * p := by simp [toIcoMod_eq_add_fract_mul]

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