digits_def' — Mathlib

English

If the base b is greater than 1, then for any n > 0 the digits of n in base b are given by (n mod b) followed by digits of (n/b).

Русский

Если основание b больше 1, то для любого n > 0 цифры числа n в основание b равны (n mod b) затем цифры (n/b).

LaTeX

$$$\\forall b>1\\forall n>0\\;\\operatorname{digits}_b(n) = (n \\bmod b) \\\\;::\\; \\operatorname{digits}_b\\left(\\frac{n}{b}\\right).$$$

Lean4

theorem digits_def' : ∀ {b : ℕ} (_ : 1 < b) {n : ℕ} (_ : 0 < n), digits b n = (n % b) :: digits b (n / b)
  | 0, h => absurd h (by decide)
  | 1, h => absurd h (by decide)
  | b + 2, _ => digitsAux_def _ (by simp) _

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