div2

Mathlib.Data.Nat.Bits

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

English

div2(n) equals ⌊n/2⌋, the greatest integer less than or equal to n/2.

Русский

div2(n) равно ⌊n/2⌋, наибольшее целое число не большее n/2.

LaTeX

$$$\mathrm{div2}(n) = \left\lfloor \dfrac{n}{2} \right\rfloor$$$

Lean4

/-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2` -/
def div2 (n : ℕ) : ℕ :=
  (boddDiv2 n).2

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

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

Разделы

Аффилиация

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