digitsAux_def — Mathlib

English

The digitsAux function is defined by a recursive recipe for base-b expansion with a bound on base 2 ≤ b.

Русский

Функция digitsAux задаётся рекурсивно через разложение по основанию b при условии 2 ≤ b.

LaTeX

$$$\text{digitsAux}(b,h,n) := \text{Recurrence for base-}b\text{ digits}$$$

Lean4

theorem digitsAux_def (b : ℕ) (h : 2 ≤ b) (n : ℕ) (w : 0 < n) : digitsAux b h n = (n % b) :: digitsAux b h (n / b) :=
  by
  cases n
  · cases w
  · rw [digitsAux, digitsAux.go, digitsAux, digitsAux.go_fuel_irrel]

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