English
Taking n modulo p^i is the same as taking the first i digits of n written in base p.
Русский
Остаток от деления n на p^i равен первому i цифрам записи n в основании p.
LaTeX
$$$ n \mod p^{i} = \mathrm{ofDigits}(p, (p.digits(n)).take(i)) $$$
Lean4
/-- Interpreting as a base `p` number and modulo `p^i` is the same as taking the first `i` digits.
-/
theorem ofDigits_mod_pow_eq_ofDigits_take {p : ℕ} (i : ℕ) (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) :
ofDigits p digits % p ^ i = ofDigits p (digits.take i) := by
induction i generalizing digits with
| zero => simp [mod_one]
| succ i ih =>
cases digits with
| nil => simp
| cons hd
tl =>
rw [List.take_succ_cons, ofDigits_cons, ofDigits_cons, ← ih _ fun x hx ↦ w₁ x <| List.mem_cons_of_mem hd hx,
add_mod, mod_eq_of_lt <| lt_of_lt_of_le (w₁ hd List.mem_cons_self) (le_pow <| add_one_pos i), pow_succ',
mul_mod_mul_left, mod_eq_of_lt]
apply add_lt_of_lt_sub
apply lt_of_lt_of_le (b := p)
· exact w₁ hd List.mem_cons_self
· rw [← Nat.mul_sub]
exact Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i
