bodd_eq_bits_head — Mathlib

English

For every n ∈ ℕ, the value bodd(n) equals the first bit in the binary representation n.bits (the head of the list): bodd(n) = headI(n.bits).

Русский

Для любого n ∈ ℕ значение bodd(n) равно первому биту двоичной записи n.bits (голове списка): bodd(n) = headI(n.bits).

LaTeX

$$$$ n\\bodd = n.bits.headI $$$$

Lean4

theorem bodd_eq_bits_head (n : ℕ) : n.bodd = n.bits.headI := by
  induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [bodd_bit, bits_append_bit _ _ h]

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