lt_digits_length_iff — Mathlib

English

For any base b and m ≠ 0, the last digit of the base-b expansion of m is nonzero.

Русский

Для основания b и m ≠ 0 последняя цифра записи m в системе b не равна нулю.

LaTeX

$$$\\forall b\\in\\mathbb{N},\\; \\forall m\\in\\mathbb{N},\\; m \\neq 0 \\Rightarrow (\\mathrm{digits}\\ b\\ m).\\mathrm{getLast} \\neq 0$$$

Lean4

theorem lt_digits_length_iff {b k : ℕ} (hb : 1 < b) (n : ℕ) : k < (b.digits n).length ↔ b ^ k ≤ n :=
  by
  rw [← not_iff_not]
  push_neg
  exact digits_length_le_iff hb n

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