English
For any base b and list L = [a0, a1, ..., a_{k-1}], the value of Nat.ofDigits b L equals the sum of a_i b^i with i from 0 to k-1.
Русский
Для основания b и списка цифр L = [a0, a1, ..., a_{k-1}] значение Nat.ofDigits b L равно сумме a_i b^i по i=0..k-1.
LaTeX
$$$\\mathrm{Nat.ofDigits}\\ b\\ L = \\sum_{i=0}^{|L|-1} a_i b^{i}$, если $L=[a_0,\\dots,a_{|L|-1}]$.$$
Lean4
theorem ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) : ofDigits b L = (L.mapIdx fun i a => a * b ^ i).sum :=
by
rw [List.mapIdx_eq_zipIdx_map, List.zipIdx_eq_zip_range', List.map_zip_eq_zipWith, ofDigits_eq_foldr, ←
List.range_eq_range']
induction L with
| nil => simp
| cons hd tl hl => simpa [List.range_succ_eq_map, List.zipWith_map_right, ofDigits_eq_sum_mapIdx_aux] using Or.inl hl
