digits_of_two_le_of_pos — Mathlib

English

For any base b with b ≥ 2 and any positive n, the digits of n in base b are given by n mod b followed by the digits of n divided by b.

Русский

Для основания b ≥ 2 и любого положительного n цифры числа n в основании b равны n mod b идущему впереди цифр digits_b(n/b).

LaTeX

$$$\\forall b\\forall n\\;\\bigl(2 \\le b \\land 0 < n \\Rightarrow \\operatorname{digits}_b(n) = n \\bmod b \\\\;::\\; \\operatorname{digits}_b\\left(\\frac{n}{b}\\right)\\bigr).$$$

Lean4

@[simp]
theorem digits_of_two_le_of_pos {b : ℕ} (hb : 2 ≤ b) (hn : 0 < n) : Nat.digits b n = n % b :: Nat.digits b (n / b) := by
  rw [Nat.eq_add_of_sub_eq hb rfl, Nat.eq_add_of_sub_eq hn rfl, Nat.digits_add_two_add_one]

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