ofDigits_eq_foldr — Mathlib

English

The value of a digit list L in base b is equal to folding L from the right with the rule (x, y) -> x + b y, starting from 0.

Русский

Значение списка цифр L в основе b равно свёртке справа по правилу (x, y) → x + b y, начиная с 0.

LaTeX

$$$\\operatorname{ofDigits}(b,L) = \\mathrm{foldr}\\bigl(\\lambda x,y.\\; x + b y\\bigr) 0\\; L.$$$

Lean4

theorem ofDigits_eq_foldr {α : Type*} [Semiring α] (b : α) (L : List ℕ) :
    ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L := by
  induction L with
  | nil => rfl
  | cons d L ih => dsimp [ofDigits]; rw [ih]

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