bit_decomp

Mathlib.Data.Int.Bitwise

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

English

Every integer n equals bit(bodd(n))(div2(n)).

Русский

Каждое целое число n равно bit(bodd(n))(div2(n)).

LaTeX

$$$$ n = \operatorname{bit}(\operatorname{bodd} n)(\operatorname{div2} n). $$$$

Lean4

theorem bit_decomp (n : ℤ) : bit (bodd n) (div2 n) = n :=
  (bit_val _ _).trans <| (add_comm _ _).trans <| bodd_add_div2 _

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

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

Разделы

Аффилиация

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