fract_sub_self

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.fract_sub_self

English

The fractional part minus the original number equals the negation of the floor: fract(a) − a = −⌊a⌋.

Русский

Дробная часть минус число равно отрицанию целой части: fract(a) − a = −⌊a⌋.

LaTeX

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

Lean4

@[simp]
theorem fract_sub_self (a : R) : fract a - a = -⌊a⌋ :=
  sub_sub_cancel_left _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru