digitsAux0 — Mathlib

English

An auxiliary construction for representing base-b digits of natural numbers, used to define the digits function.

Русский

Вспомогательное построение для получения цифр числа в основании b, используемое для определения digits.

LaTeX

$$$\text{digitsAux} : \mathbb{N} \to \mathsf{List}(\mathbb{N})$$$

Lean4

/-- (Impl.) An auxiliary definition for `digits`, to help get the desired definitional unfolding. -/
def digitsAux0 : ℕ → List ℕ
  | 0 => []
  | n + 1 => [n + 1]

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