bodd_add_div2

Mathlib.Data.Nat.Bits

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

← MathLib Explorer

English

For all n, (bodd(n)).toNat + 2 * div2(n) = n.

Русский

Для всех n: (bodd(n)).toNat + 2 * div2(n) = n.

LaTeX

$$$(\mathrm{bodd}(n)).{toNat} + 2 \cdot \mathrm{div2}(n) = n$$$

Lean4

theorem bodd_add_div2 : ∀ n, (bodd n).toNat + 2 * div2 n = n
  | 0 => rfl
  | succ n => by
    simp only [bodd_succ, div2_succ, Nat.mul_comm]
    refine Eq.trans ?_ (congr_arg succ (bodd_add_div2 n))
    cases bodd n
    · simp
    · simp; cutsat

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

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

Разделы

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

Аффилиация

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