fract_int

Mathlib.Algebra.Order.Floor.Defs

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

English

The fractional part of an integer is zero: fract(z) = 0 for all z ∈ ℤ.

Русский

Дробная часть целого числа равна нулю: fract(z) = 0 для всех z ∈ ℤ.

LaTeX

$$$\forall z \in \mathbb{Z},\; \operatorname{fract}(z) = 0.$$$

Lean4

@[simp]
theorem fract_int : (Int.fract : ℤ → ℤ) = 0 :=
  funext fun x => by simp [fract]

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

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

Разделы

Аффилиация

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