English
For fixed b and f, if two digit lists have the same length, then the lengths of the results of toDigitsCore with these lists are equal.
Русский
Для фиксированных b и f, если два списока цифр имеют одинаковую длину, то длины результатов toDigitsCore равны.
LaTeX
$$$ \forall b,f,n,l1,l2:\ (\mathrm{length}(l1)=\mathrm{length}(l2)) \Rightarrow (\mathrm{length}(b.toDigitsCore\ f\ n\ l1) = \mathrm{length}(b.toDigitsCore\ f\ n\ l2)) $$$
Lean4
/-- `n` modulo `p^i` is like taking the least significant `i` digits of `n` in base `p`.
-/
theorem self_mod_pow_eq_ofDigits_take {p : ℕ} (i n : ℕ) (h : 2 ≤ p) : n % p ^ i = ofDigits p ((p.digits n).take i) :=
by
convert ofDigits_mod_pow_eq_ofDigits_take i (zero_lt_of_lt h) (p.digits n) (fun l hl ↦ digits_lt_base h hl)
exact (ofDigits_digits p n).symm
