digits_length_le_iff — Mathlib

English

For base b>1 and n, k < (b.digits n).length iff b^k ≤ n.

Русский

Для основания b>1 и n: k < длина(b.digits n) эквивалентно b^k ≤ n.

LaTeX

$$$\\forall {b k : \\mathbb{N}},\\ 1 < b \\Rightarrow k < (b.digits n).length \\iff b^{k} \\le n$$$

Lean4

theorem digits_length_le_iff {b k : ℕ} (hb : 1 < b) (n : ℕ) : (b.digits n).length ≤ k ↔ n < b ^ k :=
  by
  by_cases h : n = 0
  · have : 0 < b ^ k := by positivity
    simpa [h]
  rw [digits_len b n hb h, ← log_lt_iff_lt_pow hb h]
  exact add_one_le_iff

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