div2_val

Mathlib.Data.Int.Bitwise

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

English

For all integers n, div2(n) = n/2 in integer division.

Русский

Для всех целых n: div2(n) = ⌊n/2⌋ (целочисленное деление).

LaTeX

$$$$ \forall n \in \mathbb{Z},\ \operatorname{div2}(n) = \left\lfloor \frac{n}{2} \right\rfloor. $$$$

Lean4

theorem div2_val : ∀ n, div2 n = n / 2
  | (n : ℕ) => congr_arg ofNat n.div2_val
  | -[n+1] => congr_arg negSucc n.div2_val

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

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

Разделы

Аффилиация

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