ofDigits_append_replicate_zero — Mathlib

English

Appending k zeros to a list does not change its interpretation by ofDigits.

Русский

Добавление k нулей к списку не изменяет значения через ofDigits.

LaTeX

$$$\\operatorname{ofDigits}(b, l ++ \\operatorname{List.replicate}(k,0)) = \\operatorname{ofDigits}(b, l).$$$

Lean4

@[simp]
theorem ofDigits_append_replicate_zero {b k : ℕ} (l : List ℕ) : ofDigits b (l ++ List.replicate k 0) = ofDigits b l :=
  by
  rw [ofDigits_append]
  simp

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