Theorems · Theorem · number theory

Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digits

∀ {p : ℕ} (L : List ℕ) {h_nonempty : L ≠ []},
  L.getLast h_nonempty ≠ 0 →
    (∀ l ∈ L, l < p) → (p - 1) * ∑ i ∈ Finset.range L.length, Nat.ofDigits p L / p ^ i.succ = Nat.ofDigits p L - L.sum

Defined in

Mathlib.Data.Nat.Digits.Lemmas

Cited by

1 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound