ofDigits — Mathlib

English

The value of a digit sequence L in base b is the unique α-valued sum L_0 + b L_1 + b^2 L_2 + ... when L = [L_0, L_1, ...].

Русский

Значение последовательности цифр L в основании b равно сумма L_0 + b L_1 + b^2 L_2 + ... для списка L = [L_0, L_1, ...].

LaTeX

$$$\\operatorname{ofDigits}(b,L) = \\sum_{i=0}^{|L|-1} L_i \\, b^{i}.$$$

Lean4

/-- `ofDigits b L` takes a list `L` of natural numbers, and interprets them
as a number in semiring, as the little-endian digits in base `b`.
-/
def ofDigits {α : Type*} [Semiring α] (b : α) : List ℕ → α
  | [] => 0
  | h :: t => h + b * ofDigits b t

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