English
The real number associated to a digit sequence is the sum of its terms: ofDigits digits = ∑' n, ofDigitsTerm digits n.
Русский
Вещественное число, соответствующее последовательности цифр, есть сумма её членов: ofDigits digits = ∑' n, ofDigitsTerm digits n.
LaTeX
$$$\mathrm{Real.ofDigits}\;: {b : \mathbb{N}} \to (\mathbb{N} \to \mathrm{Fin}\, b) \to \mathbb{R}$, \displaystyle \mathrm{ofDigits}(b)(\text{digits}) = \sum_{n=0}^{\infty} \mathrm{Real.ofDigitsTerm}(b)(\text{digits})(n)$$
Lean4
/-- `ofDigits d` is the real number `0.d₀d₁d₂...` in base `b`.
We allow repeating representations like `0.999...` here. -/
noncomputable def ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ :=
∑' n, ofDigitsTerm digits n
