Nat.three_dvd_iff
theorem Nat.three_dvd_iff : ∀ (n : ℕ), 3 ∣ n ↔ 3 ∣ (Nat.digits 10 n).sum
This is the "Divisibility by 3 Rule" theorem. It states that for any natural number 'n', the number is divisible by 3 if and only if the sum of its digits (when expressed in base 10) is divisible by 3.
More concisely: A natural number 'n' is divisible by 3 if and only if the sum of its digits, when expressed in base 10, is divisible by 3.
|
Nat.digits_add_two_add_one
theorem Nat.digits_add_two_add_one :
∀ (b n : ℕ), (b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
This theorem states that for any two natural numbers `b` and `n`, the digits of `n + 1` in base `b + 2` are obtained by adding `(n + 1) % (b + 2)` to the front of the digits of `(n + 1) / (b + 2)` in the same base. Essentially, it describes how the digits of a number in a given base can be computed by repeatedly dividing the number by the base and taking the remainder.
More concisely: For any natural number `n` and base `b`, the digits of `n + 1` in base `b + 2` are obtained by appending the remainder of `(n + 1) / (b + 2)` to the base `b+2` representation of `(n + 1) / (b + 2)`.
|
Nat.digits_lt_base'
theorem Nat.digits_lt_base' : ∀ {b m d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
The theorem `Nat.digits_lt_base'` asserts that for any natural numbers `b`, `m`, and `d`, if `d` is a digit in the base `b+2` expansion of `m`, then `d` is less than `b+2`. That's to say, every digit in the base `b+2` representation of `m` will be strictly less than `b+2`.
More concisely: For any natural numbers $m$ and base $b$, every digit $d$ in the base $b+2$ expansion of $m$ satisfies $d < b+2$.
|
Nat.ofDigits_div_pow_eq_ofDigits_drop
theorem Nat.ofDigits_div_pow_eq_ofDigits_drop :
∀ {p : ℕ} (i : ℕ),
0 < p →
∀ (digits : List ℕ),
(∀ l ∈ digits, l < p) → Nat.ofDigits p digits / p ^ i = Nat.ofDigits p (List.drop i digits)
The theorem `Nat.ofDigits_div_pow_eq_ofDigits_drop` states that for any positive integer `p` (serving as a base), any non-negative integer `i`, and any list of natural numbers `digits` where all elements are less than `p`, interpreting `digits` as a base `p` number and dividing by `p^i` is equivalent to dropping the first `i` elements from `digits` and then interpreting the resulting list as a base `p` number.
More concisely: For any base `p`, integer `i`, and base `p` number list `digits` with all elements less than `p`, the expression `(∑ j in finset.tabulate (λ k, digits!k * (p ^ (-k)), range 0 < i) / p ^ i = (drop i digits).to_nat` holds.
|
Nat.lt_base_pow_length_digits'
theorem Nat.lt_base_pow_length_digits' : ∀ {b m : ℕ}, m < (b + 2) ^ ((b + 2).digits m).length
This theorem states that for any natural numbers `b` and `m`, the number `m` is less than `(b + 2)` raised to the power of the number of digits in the representation of `m` in base `b + 2`. In other words, any number `m` is always less than the base `(b + 2)` raised to the number of digits when `m` is written in that base.
More concisely: For any natural number `m` and base `b + 2`, the value of `m` is less than `(b + 2) ^ (number of digits in base `b + 2` representation of `m`)`.
|
Nat.digits_ne_nil_iff_ne_zero
theorem Nat.digits_ne_nil_iff_ne_zero : ∀ {b n : ℕ}, b.digits n ≠ [] ↔ n ≠ 0
This theorem states that for any two natural numbers `b` and `n`, the list of digits of `n` in base `b` is not empty if and only if `n` is not zero. Essentially, it connects the mathematical concepts of numeral representation and non-zero numbers, specifying that a number has a non-empty digit representation in any base if and only if the number itself is not zero.
More concisely: For any base b and natural number n, the list of digits representing n is non-empty if and only if n is non-zero.
|
Nat.repr_length
theorem Nat.repr_length : ∀ (n e : ℕ), 0 < e → n < 10 ^ e → n.repr.length ≤ e
The theorem `Nat.repr_length` states that for any natural numbers `n` and `e`, if `e` is positive and `n` is less than 10 raised to the power `e`, then the length of the string representation of `n` (obtained using the core implementation of `Nat.repr`) is less than or equal to `e`. In other words, the length of the decimal string representation of any natural number less than a power of 10 is always less than or equal to the exponent of that power. For instance, any number less than 1000 (which is 10 to the power of 3) will have a decimal string representation of length 3 or less.
More concisely: For any natural numbers n and e, if e > 0 and n < 10^e, then the length of the decimal representation of n is less than or equal to e.
|
Nat.base_pow_length_digits_le'
theorem Nat.base_pow_length_digits_le' : ∀ (b m : ℕ), m ≠ 0 → (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m := by
sorry
This theorem states that for any non-zero natural number `m` and any base `b`, the number `m` is always greater than or equal to the base `b+2` raised to the power of the number of digits minus 1 in the base `b+2` representation of `m`. In other words, if you write `m` in base `b+2` and count the digits, then `(b+2)` to the power of that count minus 1 will always be less than or equal to `(b + 2) * m`.
More concisely: For any non-zero natural number `m` and base `b`, the number `m` is greater than or equal to `(b + 2) ^ (number of digits in base `b+2` representation of `m` - 1)`.
|
Nat.ofDigits_one
theorem Nat.ofDigits_one : ∀ (L : List ℕ), Nat.ofDigits 1 L = L.sum
This theorem states that for any list `L` of natural numbers, when the list is interpreted as the little-endian digits in base `1` using the function `Nat.ofDigits`, the result is the same as the sum of the numbers in the list `L` as computed by the `List.sum` function. In other words, when the base is `1`, the value of a number represented by a list of digits is simply the sum of the digits.
More concisely: For any list of natural numbers `L`, the sum of the numbers in `L` equals the number represented by `L` as little-endian digits in base 1, using the function `Nat.ofDigits`.
|
Nat.ofDigits_lt_base_pow_length
theorem Nat.ofDigits_lt_base_pow_length :
∀ {b : ℕ} {l : List ℕ}, 1 < b → (∀ x ∈ l, x < b) → Nat.ofDigits b l < b ^ l.length
This theorem asserts that for a given base `b` and a list `l` of natural numbers, if `b` is greater than 1 and every element `x` of the list `l` is less than `b`, then the number created by interpreting the list `l` as the little-endian digits in base `b` is less than `b` raised to the power of the length of the list `l`. Essentially, an `n`-digit number in base `b` is less than `b` to the power of `n` under these conditions.
More concisely: For any base `b` greater than 1 and list `l` of natural numbers where every element is less than `b`, the base `b` representation of `l` as a little-endian number is strictly less than `b` raised to the power of the list's length.
|
Nat.digits_zero
theorem Nat.digits_zero : ∀ (b : ℕ), b.digits 0 = []
This theorem states that for any natural number `b`, the list of digits in base `b` representation of the number `0` is an empty list. In other words, when you convert the number zero into any base `b`, the result is an empty list of digits, as the number zero does not have any digits in any base.
More concisely: For all natural numbers b, the base-b representation of the number 0 is the empty list.
|
Nat.base_pow_length_digits_le
theorem Nat.base_pow_length_digits_le : ∀ (b m : ℕ), 1 < b → m ≠ 0 → b ^ (b.digits m).length ≤ b * m
This theorem states that for any non-zero natural number `m` and any natural number `b` where `b` is greater than 1, the value of `b` raised to the power of the number of digits in the base `b` representation of `m` minus 1 is less than or equal to `b` times `m`. In other words, `m` is always larger than or equal to `b` to the power of (`number of its digits in base `b` - 1), thus providing a lower bound on the value of `m` in terms of its number of digits and the base.
More concisely: For any non-zero natural number `m` and base `b` > 1, `b` raised to the power of the number of digits in the base `b` representation of `m` - 1 is less than or equal to `bm`.
|
Nat.ofDigits_lt_base_pow_length'
theorem Nat.ofDigits_lt_base_pow_length' :
∀ {b : ℕ} {l : List ℕ}, (∀ x ∈ l, x < b + 2) → Nat.ofDigits (b + 2) l < (b + 2) ^ l.length
This theorem states that for any natural number `b` and a list `l` of natural numbers, if each element `x` in the list `l` is less than `b + 2`, then the number formed by interpreting the list `l` as the little-endian digits in base `b + 2`, is less than `(b + 2) ^ l.length`. In other words, an `n`-digit number in base `b + 2` is less than `(b + 2) ^ n`, where `n` is the length of the list `l`.
More concisely: For any natural number `b` and list `l` of natural numbers with length `n` such that each element `x` in `l` is less than `b + 2`, the base `b + 2` representation of the concatenated digits of `l` is less than `(b + 2) ^ n`.
|
Nat.ofDigits_digits
theorem Nat.ofDigits_digits : ∀ (b n : ℕ), Nat.ofDigits b (b.digits n) = n
The theorem `Nat.ofDigits_digits` asserts that for any pair of natural numbers `b` and `n`, when we convert `n` into a list of digits `Nat.digits` in base `b` and then interpret this list of digits as a number in base `b` using `Nat.ofDigits`, we get back the original number `n`. In other words, it shows that the processes of digit extraction and reconstruction in base `b` are inverse to each other. This ensures the correctness of the base `b` digit operations in the natural number context.
More concisely: For any base `b` and natural number `n`, `Nat.ofDigits b (Nat.digits n) = n`.
|
Nat.lt_base_pow_length_digits
theorem Nat.lt_base_pow_length_digits : ∀ {b m : ℕ}, 1 < b → m < b ^ (b.digits m).length
This theorem states that for any two natural numbers `b` and `m`, where `b` is greater than 1, `m` is less than `b` raised to the power of the number of digits in the base `b` representation of `m`. In other words, given a base `b` and a number `m`, when `m` is expressed in base `b`, the number of digits in this representation is an upper bound on the logarithm base `b` of `m`.
More concisely: For any base `b` and natural number `m` with `b > 1`, the number of digits in the base `b` representation of `m` is an upper bound on the logarithm base `b` of `m`.
|
Nat.to_digits_core_length
theorem Nat.to_digits_core_length :
∀ (b : ℕ), 2 ≤ b → ∀ (f n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
This theorem, `Nat.to_digits_core_length`, states that for any base `b` that is greater than or equal to 2, and for any natural numbers `f`, `n`, and `e` such that `n` is less than `b` to the power of `e` and `e` is greater than 0, the length of the string representation produced by the `toDigitsCore` function applied to `b`, `f`, `n`, and an empty list is less than or equal to `e`. This theorem holds for any base greater than one, making it applicable to binary, decimal, and hexadecimal number systems.
More concisely: For any base `b` greater than 1 and natural numbers `f`, `n`, and `e` with `n < b^e` and `e > 0`, the length of the digit representation of `n` in base `b` using `toDigitsCore` function is less than or equal to `e`.
|
Nat.self_div_pow_eq_ofDigits_drop
theorem Nat.self_div_pow_eq_ofDigits_drop :
∀ {p : ℕ} (i n : ℕ), 2 ≤ p → n / p ^ i = Nat.ofDigits p (List.drop i (p.digits n))
This theorem states that dividing a number `n` by `p` to the power of `i` is equivalent to truncating the first `i` digits of `n` when represented in base `p`. Here, `p` is a natural number greater than or equal to 2, and `i` and `n` are any natural numbers. The function `Nat.ofDigits p` is used to convert a list of digits in base `p` back into a natural number, and `List.drop i` is used to remove the first `i` digits from the list of `p`'s digits of `n`.
More concisely: For any natural numbers `n`, `p` (with `p` greater than or equal to 2), and `i`, the expression `p^i * (trunc (n / (pow p i)))` equals `Nat.ofDigits p (List.drop i (map Nat.digit p n))`.
|
Nat.digits_lt_base
theorem Nat.digits_lt_base : ∀ {b m d : ℕ}, 1 < b → d ∈ b.digits m → d < b
This theorem states that for any base `b` greater than 1, any number `n` and any digit `d`, if `d` is a digit in the base `b` expansion of `n`, then `d` is less than `b`. In other words, when a number is expressed in a base `b` representation, all of its digits will be strictly less than the base `b`.
More concisely: For any base `b` greater than 1 and any number `n` expressed in base `b`, each digit `d` in its representation satisfies `0 <= d < b`.
|
Nat.ofDigits_div_eq_ofDigits_tail
theorem Nat.ofDigits_div_eq_ofDigits_tail :
∀ {p : ℕ},
0 < p → ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → Nat.ofDigits p digits / p = Nat.ofDigits p digits.tail
This theorem states that, for any positive base `p` and a list of digits `digits` where each digit is less than `p`, interpreting the list `digits` as a number in base `p` and then dividing by `p` is equivalent to interpreting the tail of the list `digits` as a number in base `p`. In other words, discarding the least significant digit in the base `p` representation of a number is the same as dividing the number by `p`.
More concisely: For any positive base `p` and list `digits` of length `n+1` such that each digit is less than `p`, the number represented by `digits` is equivalent to `(sum (list.map (λ i, pow p i) digits) / p)` + the number represented by the tail of `digits`.
|