bit1_bits — Mathlib

English

Let n ∈ ℕ. The binary representation of 2n+1 starts with a true bit followed by the binary representation of n: (2n+1).bits = true :: n.bits.

Русский

Пусть n ∈ ℕ. Двоичное представление числа 2n+1 начинается с единицы, за которой следует представление n: (2n+1).bits = true :: n.bits.

LaTeX

$$$$ (2n + 1).bits = true :: n.bits $$$$

Lean4

@[simp]
theorem bit1_bits (n : ℕ) : (2 * n + 1).bits = true :: n.bits :=
  bits_append_bit n true fun _ => rfl

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