lt_base_pow_length_digits — Mathlib

English

If m>0 and b>1, then the digits of b·m are the same as 0 followed by the digits of m.

Русский

Если m>0 и b>1, то цифры b·m равны 0 :: цифры m.

LaTeX

$$$ \mathrm{digits}(b, b\cdot m) = 0 \,::\, \mathrm{digits}(b,m) $$$

Lean4

/-- Any number m is less than b^(number of digits in the base b representation of m) -/
theorem lt_base_pow_length_digits {b m : ℕ} (hb : 1 < b) : m < b ^ (digits b m).length :=
  by
  rcases b with (_ | _ | b) <;> try simp_all
  exact lt_base_pow_length_digits'

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