div2_succ

Mathlib.Data.Nat.Bits

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

← MathLib Explorer

English

div2(n+1) = if bodd(n) then succ(div2(n)) else div2(n).

Русский

div2(n+1) = если bodd(n), то succ(div2(n)), иначе div2(n).

LaTeX

$$$\mathrm{div2}(n+1) = \mathrm{cond}(\mathrm{bodd}(n), \mathrm{succ}(\mathrm{div2}(n)), \mathrm{div2}(n))$$$

Lean4

@[simp]
theorem div2_succ (n : ℕ) : div2 (n + 1) = cond (bodd n) (succ (div2 n)) (div2 n) :=
  by
  simp only [bodd, boddDiv2, div2]
  rcases boddDiv2 n with ⟨_ | _, _⟩ <;> simp

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

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

Разделы

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

Аффилиация

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