ofDigits_reverse_cons — Mathlib

English

The digits of the reverse of a list formed by adding a digit at front relate to the difference of reversed parts with a power term.

Русский

Цифры обратного списка, полученного добавлением цифры в начало, равны сумме цифр обратного хвоста плюс степени основания на длину хвоста, умноженной на новую цифру.

LaTeX

$$$\\operatorname{ofDigits}(b, (d :: l)^{\\mathrm{rev}}) = \\operatorname{ofDigits}(b, l^{\\mathrm{rev}}) + b^{|l|} \\; d.$$$

Lean4

theorem ofDigits_reverse_cons {b : ℕ} (l : List ℕ) (d : ℕ) :
    ofDigits b (d :: l).reverse = ofDigits b l.reverse + b ^ l.length * d :=
  by
  simp only [List.reverse_cons]
  rw [ofDigits_append]
  simp

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