digits_eq_cons_digits_div — Mathlib

English

For base b > 1 and n ≠ 0, the digits satisfy digits_b n = (n mod b) :: digits_b (n / b).

Русский

При основание b > 1 и n ≠ 0 цифры удовлетворяют digits_b n = (n mod b) :: digits_b (n / b).

LaTeX

$$$\\forall b\\,\\forall n\\,(1 < b)\\land (n \\neq 0)\\Rightarrow \\operatorname{digits}_b n = (n \\bmod b) :: \\operatorname{digits}_b(n/b).$$$

Lean4

theorem digits_eq_cons_digits_div {b n : ℕ} (h : 1 < b) (w : n ≠ 0) : digits b n = (n % b) :: digits b (n / b) :=
  digits_def' h (Nat.pos_of_ne_zero w)

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