toIcoMod_zero_one — Mathlib

English

Let α be a suitably ordered field with a floor operation. Then reducing any element b modulo the unit interval [0,1) yields its fractional part; equivalently, b can be written as b = n + fract(b) for a unique integer n and fract(b) ∈ [0,1).

Русский

Пусть α — упорядоченное поле с функцией floor. Тогда представление элемента b по модулю единичного интервала [0,1) даёт дробную часть b; то есть существует уникальное число n ∈ ℤ и дробная часть fract(b) ∈ [0,1) такое, что b = n + fract(b).

LaTeX

$$$\operatorname{fract}(b) = b - \lfloor b \rfloor$$$

Lean4

theorem toIcoMod_zero_one (b : α) : toIcoMod (zero_lt_one' α) 0 b = Int.fract b := by simp [toIcoMod_eq_add_fract_mul]

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