ofDigits_append — Mathlib

English

The value of concatenating two digit lists L1 and L2 equals ofDigits(b,L1) plus b^{|L1|} times ofDigits(b,L2).

Русский

Значение конкатенации списков цифр L1 и L2 равно ofDigits(b,L1) плюс b^{|L1|} умножить на ofDigits(b,L2).

LaTeX

$$$\\operatorname{ofDigits}(b,\, l_1 ++ l_2) = \\operatorname{ofDigits}(b, l_1) + b^{|l_1|} \\operatorname{ofDigits}(b, l_2).$$$

Lean4

theorem ofDigits_append {b : ℕ} {l1 l2 : List ℕ} :
    ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2 := by
  induction l1 with
  | nil => simp [ofDigits]
  | cons hd tl IH =>
    rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']
    ring

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