self_div_pow_eq_ofDigits_drop — Mathlib

English

Dividing n by p^i is the same as taking the digits of n and dropping i of them.

Русский

Разделение n на p^i эквивалентно взятию цифр n и удалению i из них.

LaTeX

$$$ \forall p,i:\ \forall n:\ n / p^{i} = \mathrm{ofDigits}(p, (p.digits(n)).drop(i)) $$$

Lean4

/-- Dividing `n` by `p^i` is like truncating the first `i` digits of `n` in base `p`.
-/
theorem self_div_pow_eq_ofDigits_drop {p : ℕ} (i n : ℕ) (h : 2 ≤ p) : n / p ^ i = ofDigits p ((p.digits n).drop i) :=
  by
  convert ofDigits_div_pow_eq_ofDigits_drop i (zero_lt_of_lt h) (p.digits n) (fun l hl ↦ digits_lt_base h hl)
  exact (ofDigits_digits p n).symm

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