fract_add_floor — Mathlib

English

The difference between the fractional part and the floor is the negative of the difference between the floor and the fractional part: fract(a) − ⌊a⌋ = −(⌊a⌋ − fract(a)).

Русский

Разность дробной части и целой части равна отрицанию разности целой части и дробной части: fract(a) − ⌊a⌋ = −(⌊a⌋ − fract(a)).

LaTeX

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

Lean4

@[simp]
theorem fract_add_floor (a : R) : fract a + ⌊a⌋ = a :=
  sub_add_cancel _ _

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