ofDigits_div_pow_eq_ofDigits_drop

English

Dividing by p^i corresponds to dropping i digits from the right.

Русский

Деление на p^i соответствует удалению i цифр справа.

LaTeX

$$$ \mathrm{ofDigits}(p,D) / p^{i} = \mathrm{ofDigits}(p, D.drop(i)) $$$

Lean4

/-- Interpreting as a base `p` number and dividing by `p^i` is the same as dropping `i`.
-/
theorem ofDigits_div_pow_eq_ofDigits_drop {p : ℕ} (i : ℕ) (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) :
    ofDigits p digits / p ^ i = ofDigits p (digits.drop i) := by
  induction i with
  | zero => simp
  | succ i hi =>
    rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi,
      ofDigits_div_eq_ofDigits_tail hpos (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ←
      List.drop_one, List.drop_drop, add_comm]

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