Digits of a natural number

This provides lemma about the digits of natural numbers.

theorem Nat.ofDigits_eq_sum_mapIdx_aux (b : ℕ) (l : List ℕ) : (List.zipWith (fun (a i : ℕ) => a * b ^ (i + 1)) l (List.range l.length)).sum = b * (List.zipWith (fun (a i : ℕ) => a * b ^ i) l (List.range l.length)).sum

theorem Nat.ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) : ofDigits b L = (List.mapIdx (fun (i a : ℕ) => a * b ^ i) L).sum

Properties

This section contains various lemmas of properties relating to digits and ofDigits.

theorem Nat.digits_len (b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) : (b.digits n).length = log b n + 1

theorem Nat.getLast_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) : (b.digits m).getLast ⋯ ≠ 0

theorem Nat.digits_append_digits {b m n : ℕ} (hb : 0 < b) : b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)

theorem Nat.digits_append_zeroes_append_digits {b k m n : ℕ} (hb : 1 < b) (hm : 0 < m) : b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ ((b.digits n).length + k) * m)

theorem Nat.digits_len_le_digits_len_succ (b n : ℕ) : (b.digits n).length ≤ (b.digits (n + 1)).length

theorem Nat.le_digits_len_le (b n m : ℕ) (h : n ≤ m) : (b.digits n).length ≤ (b.digits m).length

theorem Nat.pow_length_le_mul_ofDigits {b : ℕ} {l : List ℕ} (hl : l ≠ []) (hl2 : l.getLast hl ≠ 0) : (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l

theorem Nat.base_pow_length_digits_le' (b m : ℕ) (hm : m ≠ 0) : (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m

Any non-zero natural number m is greater than (b+2)^((number of digits in the base (b+2) representation of m) - 1)

theorem Nat.base_pow_length_digits_le (b m : ℕ) (hb : 1 < b) : m ≠ 0 → b ^ (b.digits m).length ≤ b * m

Any non-zero natural number m is greater than b^((number of digits in the base b representation of m) - 1)

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

theorem Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : ℕ} (n : ℕ) : (p - 1) * ∑ i ∈ Finset.range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Binary

theorem Nat.digits_two_eq_bits (n : ℕ) : digits 2 n = List.map (fun (b : Bool) => bif b then 1 else 0) n.bits

Modular Arithmetic

theorem Nat.dvd_ofDigits_sub_ofDigits {α : Type u_1} [CommRing α] {a b k : α} (h : k ∣ a - b) (L : List ℕ) : k ∣ ofDigits a L - ofDigits b L

theorem Nat.ofDigits_modEq' (b b' k : ℕ) (h : b ≡ b' [MOD k]) (L : List ℕ) : ofDigits b L ≡ ofDigits b' L [MOD k]

theorem Nat.ofDigits_modEq (b k : ℕ) (L : List ℕ) : ofDigits b L ≡ ofDigits (b % k) L [MOD k]

theorem Nat.ofDigits_mod (b k : ℕ) (L : List ℕ) : ofDigits b L % k = ofDigits (b % k) L % k

theorem Nat.ofDigits_mod_eq_head! (b : ℕ) (l : List ℕ) : ofDigits b l % b = l.head! % b

theorem Nat.head!_digits {b n : ℕ} (h : b ≠ 1) : (b.digits n).head! = n % b

theorem Nat.ofDigits_zmodeq' (b b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD ↑k]) (L : List ℕ) : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]

theorem Nat.ofDigits_zmodeq (b : ℤ) (k : ℕ) (L : List ℕ) : ofDigits b L ≡ ofDigits (b % ↑k) L [ZMOD ↑k]

theorem Nat.ofDigits_zmod (b : ℤ) (k : ℕ) (L : List ℕ) : ofDigits b L % ↑k = ofDigits (b % ↑k) L % ↑k

theorem Nat.modEq_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) : n ≡ (b'.digits n).sum [MOD b]

theorem Nat.zmodeq_ofDigits_digits (b b' : ℕ) (c : ℤ) (h : ↑b' ≡ c [ZMOD ↑b]) (n : ℕ) : ↑n ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

theorem Nat.ofDigits_neg_one (L : List ℕ) : ofDigits (-1) L = (List.map (fun (n : ℕ) => ↑n) L).alternatingSum