fract_floor

Mathlib.Algebra.Order.Floor.Ring

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

English

Let a be any element; the fractional part of its floor is zero, i.e. fract(⌊a⌋) = 0.

Русский

Пусть a произвольен; дробная часть целой части a равна нулю: fract(⌊a⌋) = 0.

LaTeX

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

Lean4

theorem fract_floor (a : R) : fract (⌊a⌋ : R) = 0 :=
  fract_intCast _

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

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

Разделы

Аффилиация

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