floor_add_fract

Mathlib.Algebra.Order.Floor.Ring

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

English

The floor of a plus its fractional part recovers the original number: ⌊a⌋ + fract(a) = a.

Русский

Целая часть числа плюс дробная часть возвращают исходное число: ⌊a⌋ + fract(a) = a.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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