English
The number formed by concatenating the base-b digits of n with the digits of m equals n plus b^{digits(n).length} times m.
Русский
Число, полученное конкатенацией цифр n и цифр m в основание b, равно n + b^{(digits(n)).length} · m.
LaTeX
$$$ \mathrm{ofDigits}(b,\mathrm{digits}(b,n)\,\mathbin{\,+}\,\mathrm{digits}(b,m)) = n + b^{\mathrm{length}(\mathrm{digits}(b,n))} \cdot m $$$
Lean4
theorem digits_base_pow_mul {b k m : ℕ} (hb : 1 < b) (hm : 0 < m) :
digits b (b ^ k * m) = List.replicate k 0 ++ digits b m := by
induction k generalizing m with
| zero => simp
| succ k ih =>
rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ, List.cons_append]
