fract_intCast

Mathlib.Algebra.Order.Floor.Ring

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

English

For any integer z, fract(z) = 0.

Русский

Для любого целого z выполняется fract(z) = 0.

LaTeX

$$\operatorname{fract}(z) = 0$$

Lean4

@[simp]
theorem fract_intCast (z : ℤ) : fract (z : R) = 0 := by
  unfold fract
  rw [floor_intCast]
  exact sub_self _

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

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

Разделы

Аффилиация

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