div2_val

Mathlib.Data.Nat.Bits

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

← MathLib Explorer

English

div2(n) equals n / 2 (integer division).

Русский

div2(n) равно n / 2 (целочисленное деление).

LaTeX

$$$\mathrm{div2}(n) = \dfrac{n}{2}$$$

Lean4

@[grind =]
theorem div2_val (n) : div2 n = n / 2 :=
  by
  refine Nat.eq_of_mul_eq_mul_left (by decide) (Nat.add_left_cancel (Eq.trans ?_ (Nat.mod_add_div n 2).symm))
  rw [mod_two_of_bodd, bodd_add_div2]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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