size — Mathlib

English

Let size(n) denote the number of bits needed to represent n in binary.

Русский

Пусть size(n) обозначает количество бит, необходимых для двоичного представления n.

LaTeX

$$$$\text{size}(0) = 0,\qquad \text{size}(n) = \left\lfloor \log_2 n \right\rfloor + 1\quad (n>0).$$$$

Lean4

/-- `size n` : Returns the size of a natural number in
bits i.e. the length of its binary representation -/
def size : ℕ → ℕ :=
  binaryRec 0 fun _ _ => succ

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