digits_base_mul — Mathlib

English

For any k≥0, digits of b^k·m are k leading zeros followed by digits of m.

Русский

Для любого k≥0 цифры b^k·m равны k ведущих нулей и далее цифры m.

LaTeX

$$$ \\mathrm{digits}(b, b^{k}\\cdot m) = \\underbrace{0,\\dots,0}_{k\\text{ times}} \\,::\, \\mathrm{digits}(b,m) $$$

Lean4

theorem digits_base_mul {b m : ℕ} (hb : 1 < b) (hm : 0 < m) : b.digits (b * m) = 0 :: b.digits m :=
  by
  rw [digits_def' hb (by positivity)]
  simp [mul_div_right m (by positivity)]

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