digits_append_zeroes_append_digits

English

For any base b and list l, the identity sum of l_i b^{i+1} equals b times sum of l_i b^{i}.

Русский

Для основания b и списка l выполняется тождество: сумма l_i b^{i+1} = b сумма l_i b^{i}.

LaTeX

$$$\\sum_{i=0}^{|l|-1} l_i b^{i+1} = b \\cdot \\sum_{i=0}^{|l|-1} l_i b^{i}$$$

Lean4

theorem digits_append_zeroes_append_digits {b k m n : ℕ} (hb : 1 < b) (hm : 0 < m) :
    digits b n ++ List.replicate k 0 ++ digits b m = digits b (n + b ^ ((digits b n).length + k) * m) :=
  by
  rw [List.append_assoc, ← digits_base_pow_mul hb hm]
  simp only [digits_append_digits (zero_lt_of_lt hb), digits_inj_iff, add_right_inj]
  ring

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