oneBits — Mathlib

English

oneBits(n) returns the list of indices of active bits in the binary representation of n.

Русский

oneBits(n) возвращает список индексов активных битов в двоичном представлении n.

LaTeX

$$$\\mathrm{oneBits}(0)=[],\\quad \\mathrm{oneBits}(\\mathrm{pos}(p))=p.\\mathrm{oneBits}(0)$$$

Lean4

/-- `n.oneBits` is the list of indices of active bits in the binary representation of `n`. -/
def oneBits : Num → List Nat
  | 0 => []
  | pos p => p.oneBits 0

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