div2

Mathlib.Data.Int.Bitwise

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

English

Int.div2 is the half function on integers, yielding the integer part of n/2.

Русский

Int.div2 — это половинная функция на целых, дающая целую часть от n/2.

LaTeX

$$$\\operatorname{div2}: \\mathbb{Z} \\to \\mathbb{Z}, \\; \\operatorname{div2}(n) = \\left\\lfloor \\dfrac{n}{2} \\right\\rfloor$$$

Lean4

/-- `div2 n = n/2` -/
def div2 : ℤ → ℤ
  | (n : ℕ) => n.div2
  | -[n+1] => negSucc n.div2

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

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

Разделы

Аффилиация

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