self_sub_fract

Mathlib.Algebra.Order.Floor.Ring

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

English

The fractional part subtracted from the original number leaves the floor: a − fract(a) = ⌊a⌋.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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