one_bits — Mathlib

English

The binary representation of 1 consists of a single true bit: Nat.bits 1 = [true].

Русский

Двоичная запись числа 1 состоит из единственного истинного бита: Nat.bits 1 = [true].

LaTeX

$$$$ Nat.bits\,1 = [true] $$$$

Lean4

@[simp]
theorem one_bits : Nat.bits 1 = [true] := by
  convert bit1_bits 0
  simp
    -- TODO Find somewhere this can live.
    -- example : bits 3423 = [true, true, true, true, true, false, true, false, true, false, true, true]
    -- := by norm_num

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