digits_len_le_digits_len_succ — Mathlib

English

For any base b and list L, Nat.ofDigits b L equals the sum of a_i b^i for i from 0 to |L|-1.

Русский

Для основания b и списка L длины k: Nat.ofDigits b L = сумма a_i b^i, где L=[a_0,...,a_{k-1}].

LaTeX

$$$\\mathrm{Nat.ofDigits}\\ b\\ L = \\sum_{i=0}^{|L|-1} a_i b^{i}$, где $L=[a_0,\\dots,a_{|L|-1}]$$$

Lean4

theorem digits_len_le_digits_len_succ (b n : ℕ) : (digits b n).length ≤ (digits b (n + 1)).length :=
  by
  rcases Decidable.eq_or_ne n 0 with (rfl | hn)
  · simp
  rcases le_or_gt b 1 with hb | hb
  · interval_cases b <;> simp +arith [digits_zero_succ', hn]
  simpa [digits_len, hb, hn] using log_mono_right (le_succ _)

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