digits_add_two_add_one — Mathlib

English

Let b and n be natural numbers. Then the digits of n+1 in base b+2 are given by the remainder of (n+1) modulo (b+2) followed by the digits of ((n+1) div (b+2)).

Русский

Пусть b и n — натуральные числа. Тогда цифры числа n+1 в основание b+2 задаются как остаток от деления (n+1) на (b+2) идущий первым элементом, за которым следуют цифры ((n+1) / (b+2)).

LaTeX

$$$\\operatorname{digits}_{b+2}(n+1) = (n+1) \\bmod (b+2) \\,::\\, \\operatorname{digits}_{b+2}\\left(\\frac{n+1}{b+2}\\right).$$$

Lean4

theorem digits_add_two_add_one (b n : ℕ) :
    digits (b + 2) (n + 1) = ((n + 1) % (b + 2)) :: digits (b + 2) ((n + 1) / (b + 2)) := by
  simp [digits, digitsAux_def]

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