digits_of_lt — Mathlib

English

If 0 < x < b, then the digits of x in base b form the one-element list [x].

Русский

Если 0 < x < b, то цифры x в основание b формируют однородный одноэлементный список [x].

LaTeX

$$$0 < x < b \\Rightarrow \\operatorname{digits}_b(x) = [x].$$$

Lean4

@[simp]
theorem digits_of_lt (b x : ℕ) (hx : x ≠ 0) (hxb : x < b) : digits b x = [x] :=
  by
  rcases exists_eq_succ_of_ne_zero hx with ⟨x, rfl⟩
  rcases Nat.exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩
  rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]

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