English
For any base b and list l = [a0, a1, ..., a_{k-1}], the sum of a_i b^{i+1} over i equals b times the sum of a_i b^{i} over i.
Русский
Для основания b и списка цифр l = [a0, a1, ..., a_{k-1}] сумма a_i b^{i+1} по i равна b умножить на сумму a_i b^{i} по i.
LaTeX
$$$\\sum_{i=0}^{|l|-1} a_i b^{i+1} = b \\cdot \\sum_{i=0}^{|l|-1} a_i b^{i}$,\nгде $l=[a_0,a_1,\\dots,a_{|l|-1}]$.$$
Lean4
theorem ofDigits_eq_sum_mapIdx_aux (b : ℕ) (l : List ℕ) :
(l.zipWith ((fun a i : ℕ => a * b ^ (i + 1))) (List.range l.length)).sum =
b * (l.zipWith (fun a i => a * b ^ i) (List.range l.length)).sum :=
by
suffices
l.zipWith (fun a i : ℕ => a * b ^ (i + 1)) (List.range l.length) =
l.zipWith (fun a i => b * (a * b ^ i)) (List.range l.length)
by simp [this]
congr; ext; ring
