ofDigits_div_eq_ofDigits_tail — Mathlib

English

Dividing the number represented by digits by p is the same as interpreting the tail of the digits.

Русский

Деление числа, записанного цифрами, на p эквивалентно интерпретации хвоста цифр.

LaTeX

$$$ \mathrm{ofDigits}(p,D) / p = \mathrm{ofDigits}(p,D.tail) $$$

Lean4

/-- Interpreting as a base `p` number and dividing by `p` is the same as interpreting the tail.
-/
theorem ofDigits_div_eq_ofDigits_tail {p : ℕ} (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) :
    ofDigits p digits / p = ofDigits p digits.tail := by
  induction digits with
  | nil => simp [ofDigits]
  | cons hd tl =>
    refine Eq.trans (add_mul_div_left hd _ hpos) ?_
    rw [Nat.div_eq_of_lt <| w₁ _ List.mem_cons_self, zero_add, List.tail_cons]

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