bit0_bits — Mathlib

English

Let n ∈ ℕ with n ≠ 0. Then the binary representation of 2n is obtained by prepending a zero bit to the binary representation of n: (2n).bits = false :: n.bits.

Русский

Пусть n ∈ ℕ и n ≠ 0. Двоичное представление числа 2n получается из представления n путём добавления слева нулевого бита: (2n).bits = false :: n.bits.

LaTeX

$$$$ (2n).bits = false :: n.bits $$$$

Lean4

@[simp]
theorem bit0_bits (n : ℕ) (hn : n ≠ 0) : (2 * n).bits = false :: n.bits :=
  bits_append_bit n false fun hn' => absurd hn' hn

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