English
The base-2 expansion digits of n coincide with the bits of n: digits 2 n equals the map of n.bits to 0/1 values.
Русский
Двоичное разложение n совпадает с последовательностью битов n: digits 2 n равно отображению n.bits в значения 0/1.
LaTeX
$$$ \\mathrm{digits} \\, 2 \\, n = \\mathrm{List}.map (\\lambda b.\\, \\text{if } b \\text{ then } 1 \\text{ else } 0) \, n.bits $$$
Lean4
theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1 0 := by
induction n using Nat.binaryRecFromOne with
| zero => simp
| one => simp
| bit b n h ih =>
rw [bits_append_bit _ _ fun hn => absurd hn h]
cases b
· rw [digits_def' one_lt_two]
· simpa [Nat.bit]
· simpa [Nat.bit, pos_iff_ne_zero]
· simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
