bit_testBit_zero_shiftRight_one

Mathlib.Data.Nat.BinaryRec

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

English

Reconstruct n from its least significant bit and the rest via testBit and shift.

Русский

Восстановление n по младшему биту и остальной части через testBit и сдвиг.

LaTeX

$$$\text{bit}(n.\text{testBit }0, n \gg 1) = n$$$

Lean4

theorem bit_testBit_zero_shiftRight_one (n : Nat) : bit (n.testBit 0) (n >>> 1) = n := by simp

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

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

Разделы

Аффилиация

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