digits_lt_base — Mathlib

English

For base b+2, every digit in the representation is strictly less than b+2.

Русский

Для основания b+2 каждая цифра в представлении строго меньше b+2.

LaTeX

$$$ \forall d\in digits(b+2,m),\ d < b+2 $$$

Lean4

/-- The digits in the base b expansion of n are all less than b, if b ≥ 2 -/
theorem digits_lt_base {b m d : ℕ} (hb : 1 < b) (hd : d ∈ digits b m) : d < b :=
  by
  rcases b with (_ | _ | b) <;> try simp_all
  exact digits_lt_base' hd

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