size_eq_bits_len — Mathlib

English

For all n ∈ ℕ, the length of the binary representation of n equals size(n).

Русский

Для всех n ∈ ℕ длина двоичного представления n равна size(n).

LaTeX

$$$|\mathrm{bits}(n)| = \operatorname{size}(n)$$$

Lean4

theorem size_eq_bits_len (n : ℕ) : n.bits.length = n.size := by
  induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h ih =>
    rw [size_bit, bits_append_bit _ _ h]
    · simp [ih]
    · simpa [bit_eq_zero_iff]

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