padicValRat.inv
theorem padicValRat.inv : ∀ {p : ℕ} [hp : Fact p.Prime] (q : ℚ), padicValRat p q⁻¹ = -padicValRat p q
This is a theorem about the p-adic valuation of the reciprocal of a rational number. Specifically, for any prime number `p` and any non-zero rational number `q`, the p-adic valuation of `q`'s reciprocal (`q⁻¹`) is the negation of the p-adic valuation of `q` itself. The p-adic valuation is a measure of how divisible a number is by a given prime, and this theorem shows that inverting a rational number inverts its p-adic valuation.
More concisely: For any prime number `p` and non-zero rational number `q`, the p-adic valuation of `q`'s reciprocal is the negation of the p-adic valuation of `q`.
|
sub_one_mul_padicValNat_choose_eq_sub_sum_digits'
theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits' :
∀ {p k n : ℕ} [hp : Fact p.Prime],
(p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
**Kummer's Theorem**
For any prime number `p`, and any natural numbers `k` and `n`, the product of `p - 1` and the `p`-adic valuation of the binomial coefficient of `n + k` choose `k` equals the sum of the base `p` digits of `k` plus the sum of the base `p` digits of `n`, minus the sum of the base `p` digits of `n + k`. Here, the `p`-adic valuation of a number is the highest power of `p` that divides the number, and the base `p` digits of a number are the coefficients when the number is expressed in the base `p` number system.
More concisely: For any prime number `p`, the `p`-adic valuation of the binomial coefficient `(p^(n+k) / (p^k * p^n))` is equal to the sum of the base `p` digits of `n` and `k`, minus the sum of the base `p` digits of `n+k`.
|
pow_padicValNat_dvd
theorem pow_padicValNat_dvd : ∀ {p n : ℕ}, p ^ padicValNat p n ∣ n
This theorem states that for any given natural numbers `p` and `n`, the `p` to the power of the `p`-adic valuation of `n` (which we denote as `p` to the power of `padicValNat p n`) is a divisor of `n`. In other words, `n` is divisible by `p` raised to the power of its `p`-adic valuation. In mathematical terms, it's expressed as \(p^{padicValNat\ p\ n} | n\).
More concisely: For any natural numbers `p` and `n`, `p` raised to the power of the `p`-adic valuation of `n` divides `n`. In other words, `p` to the power of `padicValNat p n` | `n`.
|
padicValRat.one
theorem padicValRat.one : ∀ {p : ℕ}, padicValRat p 1 = 0
The theorem `padicValRat.one` states that for any natural number `p`, the p-adic valuation of the rational number 1 is equal to 0. Here, the p-adic valuation is defined as the difference of the valuations of the numerator and the denominator of the rational number. In this case, since both the numerator and denominator are 1, their p-adic valuations are the same, hence their difference is 0.
More concisely: The p-adic valuation of the rational number 1 is 0.
|
padicValNat.self
theorem padicValNat.self : ∀ {p : ℕ}, 1 < p → padicValNat p p = 1
The theorem `padicValNat.self` states that for any natural number `p` greater than 1, the `p`-adic valuation of `p` itself is `1`. In other words, if `p` is a natural number that is not `0` or `1`, then the largest natural number `k` such that `p^k` divides `p` is `1`.
More concisely: For any prime number `p`, the `p`-adic valuation of `p` is equal to 1.
|
padicValRat.of_int
theorem padicValRat.of_int : ∀ {p : ℕ} {z : ℤ}, padicValRat p ↑z = ↑(padicValInt p z)
This theorem states that for any natural number `p` and any non-zero integer `z`, the `p`-adic value of `z` considered as a rational number is equal to the `p`-adic value of `z` considered as an integer. In other words, converting the integer `z` to a rational number does not change its `p`-adic value.
More concisely: For any natural number `p` and non-zero integer `z`, the `p`-adic value of `z` as a rational number equals the `p`-adic value of `z` as an integer.
|
padicValRat.mul
theorem padicValRat.mul :
∀ {p : ℕ} [hp : Fact p.Prime] {q r : ℚ},
q ≠ 0 → r ≠ 0 → padicValRat p (q * r) = padicValRat p q + padicValRat p r
This theorem, `padicValRat.mul`, states that for any prime number `p` and any two non-zero rational numbers `q` and `r`, the valuation of the product of `q` and `r` with respect to `p` is the sum of the valuation of `q` with respect to `p` and the valuation of `r` with respect to `p`. In other words, if $p$ is a prime number, and $q, r$ are non-zero rational numbers, then $v_p(qr) = v_p(q) + v_p(r)$, where $v_p$ denotes the $p$-adic valuation.
More concisely: For any prime number $p$ and non-zero rational numbers $q$ and $r$, the $p$-adic valuation of their product $v\_p(qr)$ equals the sum of the $p$-adic valuations of $q$ and $r$, $v\_p(q) + v\_p(r)$.
|
padicValNat_le_nat_log
theorem padicValNat_le_nat_log : ∀ {p : ℕ} (n : ℕ), padicValNat p n ≤ p.log n
This theorem states that for any natural numbers `p` and `n`, the `p`-adic valuation of `n` is always less than or equal to the logarithm of `n` to the base `p`. In mathematical terms, it can be denoted as `padicValNat(p, n) ≤ log_p(n)`. Here, the `p`-adic valuation of `n` is defined as the largest natural number `k` such that `p^k` divides `n`, given `p ≠ 1` and `n > 0`, otherwise it defaults to `0`. The logarithm of `n` to the base `p` is the power to which `p` must be raised to obtain `n`.
More concisely: For any natural number `n` and prime number `p`, the `p`-adic valuation of `n` is less than or equal to the logarithm base `p` of `n`. In other words, `padicValNat(p, n) ≤ log_p(n)`.
|
padicValInt.zero
theorem padicValInt.zero : ∀ {p : ℕ}, padicValInt p 0 = 0
This theorem states that for any natural number `p`, the `p`-adic valuation of `0` is `0`. In mathematical terms, this means that regardless of what `p` we choose, there is no natural number `k` such that `p^k` divides `0`, hence, the `p`-adic valuation is defaulted to `0`.
More concisely: For any prime number p, the p-adic valuation of 0 is 0.
|
padicValRat.le_padicValRat_add_of_le
theorem padicValRat.le_padicValRat_add_of_le :
∀ {p : ℕ} [hp : Fact p.Prime] {q r : ℚ},
q + r ≠ 0 → padicValRat p q ≤ padicValRat p r → padicValRat p q ≤ padicValRat p (q + r)
This theorem presents sufficient conditions to prove that the `p`-adic valuation of a rational number `q` is less than or equal to the `p`-adic valuation of the sum of `q` and another rational number `r`. Specifically, the conditions are that the sum of `q` and `r` is not zero, and the `p`-adic valuation of `q` is less than or equal to the `p`-adic valuation of `r`. If these conditions are met, it follows that the `p`-adic valuation of `q` is less than or equal to the `p`-adic valuation of `q + r`. Here, `p` is a prime number.
More concisely: If `p` is a prime number and the sum of rational numbers `q` and `r` is nonzero with `p`-adic valuation of `q` less than or equal to that of `r`, then the `p`-adic valuation of `q` is less than or equal to the `p`-adic valuation of `q + r`.
|
padicValRat.zero
theorem padicValRat.zero : ∀ {p : ℕ}, padicValRat p 0 = 0
The theorem `padicValRat.zero` states that for any natural number `p`, the p-adic valuation of the rational number `0` is `0`. In mathematical terms, it says that if you calculate the p-adic valuation of `0`, regardless of the value of `p`, the result will always be `0`.
More concisely: For any prime number p, the p-adic valuation of rational number 0 is 0.
|
padicValNat.one
theorem padicValNat.one : ∀ {p : ℕ}, padicValNat p 1 = 0
The theorem `padicValNat.one` states that for any natural number `p`, the `p`-adic valuation of `1` is `0`. In other words, for any prime number `p`, there is no power of `p` that divides `1`, and thus the maximum such power, or the `p`-adic valuation, is `0`.
More concisely: The `p`-adic valuation of the natural number 1 is 0 for any prime number `p`.
|
padicValRat.self
theorem padicValRat.self : ∀ {p : ℕ}, 1 < p → padicValRat p ↑p = 1
The theorem `padicValRat.self` states that for any natural number `p` which is greater than `1`, the p-adic valuation of `p` expressed as a rational number is `1`. The p-adic valuation, `padicValRat`, is defined as the difference between the valuations of the numerator and the denominator of the rational number. In this case, since `p` is both the numerator and the denominator, their valuations are the same, yielding a p-adic valuation of `1`.
More concisely: For any prime number `p`, the p-adic valuation of `p` as a rational number is 1.
|
padicValNat_choose'
theorem padicValNat_choose' :
∀ {p n k b : ℕ} [hp : Fact p.Prime],
p.log (n + k) < b →
padicValNat p ((n + k).choose k) =
(Finset.filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Finset.Ico 1 b)).card
**Kummer's Theorem**
Kummer's theorem, in the context of p-adic numbers, states that for a prime number `p` and natural numbers `n`, `k`, and `b` (where `b` is any bound greater than the base `p` logarithm of `n + k`), the p-adic valuation of the binomial coefficient "n + k choose k" is equal to the number of carries when `k` and `n` are added in base `p`. This number of carries can be calculated as the number of elements in the finset interval from 1 to `b` (i.e., `Ico 1 b`), where each element `i` fulfills the condition that `p` raised to the power `i` is less than or equal to the sum of `k` and `n` modulo `p` raised to the power `i`.
More concisely: Kummer's Theorem states that the p-adic valuation of the binomial coefficient "n + k choose k" equals the number of carries when adding n and k in base p, which can be calculated as the cardinality of the finset {i in [1, b] | p^i <= (k + n)^i mod p^i}.
|
padicValInt.self
theorem padicValInt.self : ∀ {p : ℕ}, 1 < p → padicValInt p ↑p = 1
This theorem states that if `p` is a natural number greater than `1`, then the `p`-adic valuation of `p` itself is `1`. In other words, for a nonzero natural number `p` not equal to `1`, the largest natural number `k` such that `p^k` divides `p` is `1`.
More concisely: For any prime natural number `p > 1`, the `p`-adic valuation of `p` is equal to 1.
|
Mathlib.NumberTheory.Padics.PadicVal._auxLemma.7
theorem Mathlib.NumberTheory.Padics.PadicVal._auxLemma.7 :
∀ {p n : ℕ}, (padicValNat p n = 0) = (p = 1 ∨ n = 0 ∨ ¬p ∣ n)
This theorem states that for any two natural numbers `p` and `n`, the `p`-adic valuation of `n` is zero if and only if either `p` equals 1, `n` equals 0, or `p` does not divide `n`. In mathematical terminology, for `p, n ∈ ℕ`, we have `padicValNat(p, n) = 0` if and only if `p = 1`, `n = 0`, or `p ∤ n`.
More concisely: The `p`-adic valuation of a natural number `n` is zero if and only if `p` is equal to 1, `n` is zero, or `p` does not divide `n`.
|
padicValNat.zero
theorem padicValNat.zero : ∀ {p : ℕ}, padicValNat p 0 = 0
The theorem `padicValNat.zero` states that for any natural number `p`, the `p`-adic valuation of `0` is `0`. This is consistent with the definition of `p`-adic valuation, which specifies that the `p`-adic valuation of `0` defaults to `0` regardless of the value of `p`.
More concisely: The `p`-adic valuation of the natural number 0 is 0.
|
padicValNat_choose
theorem padicValNat_choose :
∀ {p n k b : ℕ} [hp : Fact p.Prime],
k ≤ n →
p.log n < b →
padicValNat p (n.choose k) =
(Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)).card
**Kummer's Theorem**
Kummer's theorem states that, for a prime number `p`, and natural numbers `n`, `k`, and `b`, where `k` is less than or equal to `n` and the logarithm base `p` of `n` is less than `b`, the `p`-adic valuation of the binomial coefficient `n.choose k` is given by the number of elements in the set of integers `i` from 1 (inclusive) to `b` (exclusive) for which `p` to the power of `i` is less than or equal to the sum of the remainders of `k` and `n - k` when divided by `p` to the power of `i`. In simple terms, it is the number of carries when `k` and `n - k` are added in base `p`. This sum is summed over all `i` in the set from 1 to any bound `b` that is greater than the base `p` logarithm of `n`.
More concisely: Kummer's theorem asserts that the `p`-adic valuation of the binomial coefficient `n choose k` is equal to the number of carries when adding `k` and `n - k` in base `p` up to a bound `b`, where `p` is a prime number, `n` and `k` are natural numbers with `k` less than or equal to `n`, and the base `p` logarithm of `n` is less than `b`.
|
padicValRat.finite_int_prime_iff
theorem padicValRat.finite_int_prime_iff : ∀ {p : ℕ} [hp : Fact p.Prime] {a : ℤ}, multiplicity.Finite (↑p) a ↔ a ≠ 0
This theorem states that the multiplicity of a prime number `p` in an integer `a` is finite if and only if `a` is not equal to zero. In other words, a prime number `p` can be a factor of an integer `a` only a finite number of times, and this is true exactly when `a` is not zero.
More concisely: A prime number `p` divides an integer `a` finitely many times, i.e., the multiplicity of `p` as a divisor of `a` is finite, if and only if `a` is nonzero.
|
padicValNat_mul_div_factorial
theorem padicValNat_mul_div_factorial :
∀ {p : ℕ} (n : ℕ) [hp : Fact p.Prime], padicValNat p (p * (n / p)).factorial = padicValNat p n.factorial
The theorem `padicValNat_mul_div_factorial` states that for any natural number `p` that is prime and any natural number `n`, the `p`-adic valuation of the factorial of `n` is equal to the `p`-adic valuation of the factorial of the largest multiple of `p` that is less than or equal to `n`, which is denoted by `(p * ⌊n / p⌋)!`. In other words, when calculating the `p`-adic valuation of a factorial, we can replace the number with its greatest multiple of `p`. The `p`-adic valuation is a measurement of how many times a given prime number `p` divides a number, with the special case that if `n` is zero or `p` is one, the `p`-adic valuation defaults to zero.
More concisely: The `p`-adic valuation of `n!` equals the `p`-adic valuation of `(p * ⌊n / p⌋)!`, where `p` is a prime number and `n` is a natural number.
|
padicValNat_factorial_mul
theorem padicValNat_factorial_mul :
∀ {p : ℕ} (n : ℕ) [hp : Fact p.Prime], padicValNat p (p * n).factorial = padicValNat p n.factorial + n
The theorem `padicValNat_factorial_mul` states that for any prime number `p` and any natural number `n`, the `p`-adic valuation of the factorial of `p * n` is equal to the `p`-adic valuation of the factorial of `n` plus `n`. In mathematical terms, if `v_p` denotes the `p`-adic valuation, this theorem can be written as `v_p((p*n)!) = v_p(n!) + n`. This tells us about how the power of `p` in the prime factorization of `(p * n)!` compares to the power of `p` in the prime factorization of `n!`.
More concisely: For any prime number `p` and natural number `n`, the `p`-adic valuation of the factorial of `p * n` is equal to the `p`-adic valuation of the factorial of `n` plus `n`. In Lean notation, `v_p((p * n)!) = v_p(n!) + n`.
|
padicValRat.min_le_padicValRat_add
theorem padicValRat.min_le_padicValRat_add :
∀ {p : ℕ} [hp : Fact p.Prime] {q r : ℚ},
q + r ≠ 0 → min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)
The theorem `padicValRat.min_le_padicValRat_add` states that for any prime number `p` and any two rational numbers `q` and `r` such that their sum is not zero, the minimum of the p-adic valuations of `q` and `r` is less than or equal to the p-adic valuation of their sum. The p-adic valuation of a rational number is calculated as the valuation of its numerator minus the valuation of its denominator. In this context, valuation refers to the exponent of the prime `p` in the prime factorization of the number.
More concisely: For any prime number p and rational numbers q and r with non-zero sum, the p-adic valuation of q + r is less than or equal to the minimum of the p-adic valuations of q and r.
|
padicValRat.lt_sum_of_lt
theorem padicValRat.lt_sum_of_lt :
∀ {p j : ℕ} [hp : Fact p.Prime] {F : ℕ → ℚ} {S : Finset ℕ},
S.Nonempty →
(∀ i ∈ S, padicValRat p (F j) < padicValRat p (F i)) →
(∀ (i : ℕ), 0 < F i) → padicValRat p (F j) < padicValRat p (S.sum fun i => F i)
This theorem states that if the p-adic valuation of every positive rational in a finite nonempty set is greater than the p-adic valuation of another given positive rational, then the p-adic valuation of the sum of all the rationals in the finite set is also greater than the p-adic valuation of the given rational. Here, 'p' is a prime number, and the p-adic valuation of a rational number is defined as the valuation of its numerator minus the valuation of its denominator.
More concisely: If the p-adic valuation of every positive rational in a finite set is strictly greater than the p-adic valuation of a given positive rational, then the p-adic valuation of the sum of all rationals in the set is strictly greater than the p-adic valuation of that rational.
|
padicValRat.pow
theorem padicValRat.pow :
∀ {p : ℕ} [hp : Fact p.Prime] {q : ℚ}, q ≠ 0 → ∀ {k : ℕ}, padicValRat p (q ^ k) = ↑k * padicValRat p q
The theorem `padicValRat.pow` states that for any natural number `p` which is prime, any nonzero rational number `q`, and any natural number `k`, the p-adic valuation of `q` raised to the power `k` is equal to `k` times the p-adic valuation of `q`. In other words, we have `padicValRat p (q ^ k) = k * padicValRat p q`. This provides the property of the p-adic valuation operation being distributive over exponentiation.
More concisely: For any prime number `p`, nonzero rational number `q`, and natural number `k`, the p-adic valuation of `q` raised to the power `k` equals `k` times the p-adic valuation of `q`. (Or, more succinctly: The p-adic valuation operation is distributive over exponentiation.)
|
padicValRat.of_int_multiplicity
theorem padicValRat.of_int_multiplicity :
∀ {p : ℕ} {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0), padicValRat p ↑z = ↑((multiplicity (↑p) z).get ⋯)
The theorem `padicValRat.of_int_multiplicity` states that for any natural number `p` not equal to 1, and any integer `z` not equal to 0, the `p`-adic value of `z` is equal to the multiplicity of `p` in `z`. In other words, the `p`-adic valuation of a non-zero integer `z` is exactly the highest power of `p` that divides `z`.
More concisely: For any prime number `p` and non-zero integer `z`, the `p`-adic value of `z` equals the highest power of `p` that divides `z`.
|
padicValRat.neg
theorem padicValRat.neg : ∀ {p : ℕ} (q : ℚ), padicValRat p (-q) = padicValRat p q
The theorem `padicValRat.neg` states that the p-adic valuation function `padicValRat` is symmetric with respect to the rational number `q`. In other words, for any natural number `p` and rational number `q`, the p-adic valuation of `-q` is the same as the p-adic valuation of `q`.
More concisely: For any prime number p and rational number q, the p-adic valuation of q is equal to the p-adic valuation of -q.
|
padicValNat.eq_zero_of_not_dvd
theorem padicValNat.eq_zero_of_not_dvd : ∀ {p n : ℕ}, ¬p ∣ n → padicValNat p n = 0
This theorem states that for any two natural numbers `p` and `n`, if `p` does not divide `n`, then the `p`-adic valuation of `n` is zero. In mathematical terms, if `p` is not a divisor of `n`, denoted as ¬(p ∣ n), then the largest natural number `k` such that `p^k` divides `n` is zero, i.e., `padicValNat p n = 0`. This is because there's no power of `p` that can divide `n` when `p` itself doesn't divide `n`.
More concisely: If a prime number `p` does not divide a natural number `n`, then the `p`-adic valuation of `n` is zero.
|
padicValNat_factorial
theorem padicValNat_factorial :
∀ {p n b : ℕ} [hp : Fact p.Prime],
p.log n < b → padicValNat p n.factorial = (Finset.Ico 1 b).sum fun i => n / p ^ i
**Legendre's Theorem**
The theorem essentially states that for a given prime number `p` and a natural number `n`, the `p`-adic valuation of `n!` (the factorial of `n`) is equal to the sum of the quotients when `n` is divided by `p` raised to power `i` for each `i` in the finite set of natural numbers starting from 1 and ending before `b`. Here, `b` is any number that is greater than the largest power of `p` that divides `n`. This is a fundamental result in number theory and gives insights into the prime number factorization of a factorial.
More concisely: For any prime number `p` and natural number `n`, the `p`-adic valuation of `n!` is equal to the sum of the quotients when `n` is divided by `p` raised to power `i` for each `i` in the range `1` to the largest power of `p` that divides `n`.
|
padicValNat.proof_1
theorem padicValNat.proof_1 : ∀ (p n : ℕ), p ≠ 1 ∧ 0 < n → multiplicity.Finite p n
The theorem `padicValNat.proof_1` states that for all natural numbers `p` and `n`, if `p` is not equal to one and `n` is positive, then the multiplicity of `p` in `n` is finite. In mathematical terms, this means that there exists a natural number `m` such that `p` to the power of `(m + 1)` does not divide `n`.
More concisely: For all natural numbers p neither equal to 1 nor zero, and all positive natural numbers n, there exists a natural number m such that p^(m+1) does not divide n.
|
nat_log_eq_padicValNat_iff
theorem nat_log_eq_padicValNat_iff :
∀ {p n : ℕ} [hp : Fact p.Prime], 0 < n → (p.log n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1))
The theorem `nat_log_eq_padicValNat_iff` states that for any prime number `p` and positive natural number `n`, the logarithm of `n` with base `p` equals the `p`-adic valuation of `n` if and only if `n` is less than `p` raised to the power of one plus the `p`-adic valuation of `n`. Here, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such that `p^k` divides `n`. If `n = 0` or `p = 1`, then `padicValNat p q` defaults to `0`. The condition that `p` is prime is ensured by the typeclass instance `Fact p.Prime`.
More concisely: For any prime number $p$ and natural number $n \neq 0$, the logarithm of $n$ with base $p$ equals the $p$-adic valuation of $n$ if and only if $n = p^{val\_p(n) + 1}$, where $val\_p(n)$ is the largest natural number such that $p^{val\_p(n)}$ divides $n$.
|
padicValNat.pow
theorem padicValNat.pow :
∀ {p a : ℕ} [hp : Fact p.Prime] (n : ℕ), a ≠ 0 → padicValNat p (a ^ n) = n * padicValNat p a
This theorem states that for all prime numbers `p` and all natural numbers `a` and `n`, where `a` is not equal to zero, the p-adic valuation of `a` raised to the power of `n` is equal to `n` times the p-adic valuation of `a`. In other words, the p-adic valuation of a power of a number is just the exponent times the p-adic valuation of the original number. In more mathematical terms, if p-adicValNat is denoted as v_p, then we have v_p(a^n) = n * v_p(a) for any prime p and natural number a (where a ≠ 0).
More concisely: For any prime number p and natural number a not equal to zero, the p-adic valuation of a raised to the power of n equals n times the p-adic valuation of a. (Or equivalently, v_p(a^n) = n * v_p(a) for all prime p and natural number a with a ≠ 0.)
|
padicValNat_self
theorem padicValNat_self : ∀ {p : ℕ} [inst : Fact p.Prime], padicValNat p p = 1
The theorem `padicValNat_self` states that for every natural number `p` which is prime, the `p`-adic valuation of `p` is `1`. In other words, for a prime number `p`, there is exactly one `p` to the power of `1` that divides `p`. This makes sense as prime numbers are only divisible by `1` and themselves.
More concisely: For every prime number `p`, the `p`-adic valuation of `p` is equal to 1.
|
padicValNat.padicValNat_eq_maxPowDiv
theorem padicValNat.padicValNat_eq_maxPowDiv : padicValNat = Nat.maxPowDiv
This theorem provides a more efficient way to calculate the `p`-adic valuation of a natural number. Essentially, it states that the function `padicValNat`, which calculates the highest power `k` of a given natural number `p` that divides another natural number `n`, is equal to the function `Nat.maxPowDiv`. This equality allows for a more efficient code generation in Lean 4 when calculating `p`-adic valuations.
More concisely: The theorem asserts that the function `padicValNat` calculating the highest power of a prime `p` dividing a natural number `n` is equal to `Nat.maxPowDiv`.
|
padicValRat.div
theorem padicValRat.div :
∀ {p : ℕ} [hp : Fact p.Prime] {q r : ℚ},
q ≠ 0 → r ≠ 0 → padicValRat p (q / r) = padicValRat p q - padicValRat p r
This theorem provides a rewrite rule for the p-adic valuation of the division of two rational numbers `q` and `r`. It specifically states that for a prime number `p`, and two non-zero rational numbers `q` and `r`, the p-adic valuation of the division `q / r` is equal to the p-adic valuation of `q` minus the p-adic valuation of `r`. This gives us a way to simplify the calculation of p-adic valuations in the context of division operations.
More concisely: For prime number p and non-zero rational numbers q and r, the p-adic valuation of q/r equals the difference of the p-adic valuations of q and r.
|
padicValNat_def'
theorem padicValNat_def' : ∀ {p n : ℕ}, p ≠ 1 → 0 < n → ↑(padicValNat p n) = multiplicity p n
The theorem `padicValNat_def'` states that for any two natural numbers `p` and `n`, given that `p` is not equal to `1` and `n` is positive, the `p`-adic valuation of `n`, when converted to an infinite natural number (`PartENat`), is equal to the multiplicity of `p` in `n`. In other words, the largest exponent `k` such that `p^k` divides `n` is the same whether we compute it using the `p`-adic valuation function or the multiplicity function.
More concisely: For any prime number `p` and positive natural number `n`, the `p`-adic valuation of `n` equals the multiplicity of `p` in `n`.
|
padicValNat.div_of_dvd
theorem padicValNat.div_of_dvd :
∀ {p a b : ℕ} [hp : Fact p.Prime], b ∣ a → padicValNat p (a / b) = padicValNat p a - padicValNat p b
The theorem `padicValNat.div_of_dvd` states that for any natural numbers `p`, `a`, and `b`, where `p` is a prime number (`Nat.Prime p`), if `b` divides `a` (expressed as `b ∣ a`), then the p-adic valuation of the quotient of `a` divided by `b` (`a / b`) is equal to the difference between the p-adic valuation of `a` and the p-adic valuation of `b`. In mathematical terms, this can be represented as $\nu_p(a/b) = \nu_p(a) - \nu_p(b)$, where $\nu_p(n)$ represents the p-adic valuation of a number `n`.
More concisely: For a prime number `p`, if `b` divides `a`, then the p-adic valuation of their quotient `a / b` equals the difference between the p-adic valuations of `a` and `b`: $\nu_p(a/b) = \nu_p(a) - \nu_p(b)$.
|
sub_one_mul_padicValNat_choose_eq_sub_sum_digits
theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits :
∀ {p k n : ℕ} [hp : Fact p.Prime],
k ≤ n → (p - 1) * padicValNat p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum
**Kummer's Theorem** in Lean's theorem `sub_one_mul_padicValNat_choose_eq_sub_sum_digits` states that for any prime number `p` and natural numbers `k` and `n` where `k` is less than or equal to `n`, multiplying `p - 1` with the `p`-adic valuation of the binomial coefficient `n choose k` equals the sum of the base `p` digits of `k` plus the sum of the base `p` digits of `n - k` minus the sum of the base `p` digits of `n`. This theorem gives a relationship between the `p`-adic valuation of a binomial coefficient and the sum of digits in a certain base.
More concisely: For any prime number `p`, natural numbers `k` and `n` with `k ≤ n`, the equality `(p - 1) * v\_p(binomial n k) = s(k) + s(n - k) - s(n)`, where `v\_p` denotes the `p`-adic valuation and `s(n)` the sum of the base `p` digits of `n`.
|
padicValRat.of_nat
theorem padicValRat.of_nat : ∀ {p n : ℕ}, padicValRat p ↑n = ↑(padicValNat p n)
The theorem `padicValRat.of_nat` states that for any natural numbers `p` and `n`, the `p`-adic value of `n` when considered as an integer is the same as its `p`-adic value when considered as a rational number. Here, the `p`-adic value of a number is the highest power of `p` that divides the number, with the valuation of `0` or of any number with respect to `1` defined to be `0`. Thus, the `p`-adic valuation of a natural number is preserved under the embedding of the integers into the rationals.
More concisely: For any natural number `n` and prime number `p`, the `p`-adic valuation of `n` as an integer equals the `p`-adic valuation of the rational number `(from Nat.cast (natToInt n))`.
|
padicValRat.padicValRat_le_padicValRat_iff
theorem padicValRat.padicValRat_le_padicValRat_iff :
∀ {p : ℕ} [hp : Fact p.Prime] {n₁ n₂ d₁ d₂ : ℤ},
n₁ ≠ 0 →
n₂ ≠ 0 →
d₁ ≠ 0 →
d₂ ≠ 0 →
(padicValRat p (Rat.divInt n₁ d₁) ≤ padicValRat p (Rat.divInt n₂ d₂) ↔
∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁)
This theorem provides a condition for the valuation at a prime `p` of the rational number `(n₁ / d₁)` to be less than or equal to the valuation at `p` of the rational number `(n₂ / d₂)`. This condition is expressed in terms of divisibility by `p^n`. Specifically, the valuation at `p` of `(n₁ / d₁)` is less than or equal to the valuation at `p` of `(n₂ / d₂)` if and only if for every natural number `n`, if `p^n` divides the product `n₁ * d₂`, then `p^n` also divides the product `n₂ * d₁`. This statement assumes that `p` is a prime number and that `n₁`, `n₂`, `d₁`, `d₂` are all non-zero integers.
More concisely: The theorem states that for prime `p` and integers `n₁, n₂, d₁, d₂ ≠ 0`, `v_p(n₁/d₁) ≤ v_p(n₂/d₂)` if and only if `p^n | (n₁ * d₂) → p^n | (n₂ * d₁)` for all `n ∈ ℕ`. Here, `v_p` denotes the `p`-adic valuation.
|
sub_one_mul_padicValNat_factorial
theorem sub_one_mul_padicValNat_factorial :
∀ {p : ℕ} [hp : Fact p.Prime] (n : ℕ), (p - 1) * padicValNat p n.factorial = n - (p.digits n).sum
**Legendre's Theorem**
Legendre's Theorem states that for any prime number `p` and any natural number `n`, multiplying `p - 1` by the `p`-adic valuation of the factorial of `n` equals `n` minus the sum of the digits of `n` when it is expressed in base `p`. In other words, `(p - 1) * padicValNat p n.factorial = n - (p.digits n).sum`. The `p`-adic valuation of `n!` is the highest power of `p` that divides `n!`, and `p.digits n` is the representation of `n` in base `p`.
More concisely: For any prime number `p` and natural number `n`, the `p`-adic valuation of `n!` is equivalent to `n - sum (digit i of (p-base n) : list nat)`, where `digit` is the function returning the digit in base `p` representation.
|
padicValInt.of_nat
theorem padicValInt.of_nat : ∀ {p n : ℕ}, padicValInt p ↑n = padicValNat p n
This theorem states that for any natural numbers `p` and `n`, the `p`-adic valuation of `n` when it is considered as an integer is the same as its `p`-adic valuation when it is considered as a natural number. In other words, the process of calculating the `p`-adic valuation does not depend on whether the number `n` is treated as an integer or as a natural number, it will yield the same result in either case.
More concisely: For any natural number `n` and prime `p`, the `p`-adic valuation of `n` as an integer equals the `p`-adic valuation of `n` as a natural number.
|
padicValRat.add_eq_min
theorem padicValRat.add_eq_min :
∀ {p : ℕ} [hp : Fact p.Prime] {q r : ℚ},
q + r ≠ 0 →
q ≠ 0 →
r ≠ 0 → padicValRat p q ≠ padicValRat p r → padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
This theorem states the ultrametric property of a p-adic valuation. Specifically, given a prime number `p`, and two non-zero rational numbers `q` and `r` such that the p-adic valuation of `q` and `r` are not equal, if the sum of `q` and `r` is not zero, then the p-adic valuation of this sum is equal to the minimum of the p-adic valuation of `q` and the p-adic valuation of `r`. In mathematical terms, if `p` is prime and `q, r ∈ ℚ` are non-zero with `padicValRat p q ≠ padicValRat p r`, then provided `q + r ≠ 0`, we have `padicValRat p (q + r) = min(padicValRat p q, padicValRat p r)`.
More concisely: Given a prime number `p` and non-zero rational numbers `q` and `r` with unequal `p`-adic valuations, if their sum is non-zero, then their `p`-adic valuations are equal to the minimum of the two.
|
padicValInt.one
theorem padicValInt.one : ∀ {p : ℕ}, padicValInt p 1 = 0
The theorem `padicValInt.one` states that for any natural number `p`, the `p`-adic valuation of 1 is 0. In mathematical terms, this means that for any prime number `p`, there is no `p` to the power of any natural number that divides 1, since the highest power of any number that can divide 1 is 0. Hence, the `p`-adic valuation of 1 is always 0, irrespective of the value of `p`.
More concisely: The `p-adic valuation of 1 is 0 for all prime numbers p.`
|
padicValRat_of_nat
theorem padicValRat_of_nat : ∀ {p : ℕ} (n : ℕ), ↑(padicValNat p n) = padicValRat p ↑n
The theorem `padicValRat_of_nat` establishes that the `p`-adic valuation of a natural number `n` under a given natural number `p` is equivalent when computed through `padicValNat` and `padicValRat` functions. In other words, the `p`-adic valuation of a natural number `n` is the same whether `n` is considered as a natural number or as a rational number.
More concisely: The `p`-adic valuation of a natural number is equal to the `p`-adic valuation of the corresponding rational number.
|
padicValNat_def
theorem padicValNat_def :
∀ {p : ℕ} [hp : Fact p.Prime] {n : ℕ} (hn : 0 < n), padicValNat p n = (multiplicity p n).get ⋯
The theorem `padicValNat_def` states that for any prime number `p` and any natural number `n` greater than zero, the `p`-adic valuation of `n`, which is the largest natural number `k` such that `p^k` divides `n`, is equal to the multiplicity of `p` in `n`, i.e., the largest natural number `n` such that `p^n` divides `n`. In essence, it simplifies the calculation of the `p`-adic valuation when the input is a prime number, mirroring the definition of `padicValRat_def`.
More concisely: For any prime number p and natural number n > 0, the p-adic valuation of n equals the multiplicity of p as a divisor of n.
|
padicValNat.div
theorem padicValNat.div : ∀ {p b : ℕ} [hp : Fact p.Prime], p ∣ b → padicValNat p (b / p) = padicValNat p b - 1 := by
sorry
The theorem `padicValNat.div` states that for any prime number `p` and a natural number `b`, if `p` divides `b`, then the `p`-adic valuation of `b / p` is equal to the `p`-adic valuation of `b` minus `1`. In other words, when you divide a number by one of its prime factors, the largest power of that prime which divides the result is one less than the largest power of that prime that divided the original number.
More concisely: For any prime number p and natural number b, if p divides b then the p-adic valuation of b / p is equal to the p-adic valuation of b - 1.
|
padicValNat_eq_zero_of_mem_Ioo
theorem padicValNat_eq_zero_of_mem_Ioo : ∀ {p m k : ℕ}, m ∈ Set.Ioo (p * k) (p * (k + 1)) → padicValNat p m = 0 := by
sorry
The theorem `padicValNat_eq_zero_of_mem_Ioo` states that for any natural numbers `p`, `m`, and `k`, if `m` is in the open interval between `p * k` and `p * (k + 1)`, then the `p`-adic valuation of `m` is zero. In other words, if a natural number `m` is strictly greater than the product of `p` and `k` and strictly less than the product of `p` and `k + 1`, there exist no natural numbers `n` such that `p` to the power of `n` divides `m`. If `m = 0` or `p = 1`, then `padicValNat p m` defaults to `0`.
More concisely: If `p` is a prime number and `m` is a natural number strictly between `p * k` and `p * (k + 1)`, then the `p`-adic valuation of `m` is zero.
|
padicValRat.defn
theorem padicValRat.defn :
∀ (p : ℕ) [hp : Fact p.Prime] {q : ℚ} {n d : ℤ} (hqz : q ≠ 0) (qdf : q = Rat.divInt n d),
padicValRat p q = ↑((multiplicity (↑p) n).get ⋯) - ↑((multiplicity (↑p) d).get ⋯)
The theorem `padicValRat.defn` states that for any natural number `p` that is prime, and any rational number `q` that is not zero and can be expressed as the division of two integers `n` and `d` using `Rat.divInt`, the p-adic valuation of `q` is equal to the difference between the multiplicity of `p` in `n` and the multiplicity of `p` in `d`. Here, the multiplicity of `p` in `n` (or `d`) is the largest natural number `n` such that `p^n` divides `n` (or `d`).
More concisely: For prime number p and rational number q = n/d ≠ 0, the p-adic valuation of q is equal to the difference in the multiplicities of p dividing n and d.
|
padicValRat.sum_pos_of_pos
theorem padicValRat.sum_pos_of_pos :
∀ {p : ℕ} [hp : Fact p.Prime] {n : ℕ} {F : ℕ → ℚ},
(∀ i < n, 0 < padicValRat p (F i)) →
((Finset.range n).sum fun i => F i) ≠ 0 → 0 < padicValRat p ((Finset.range n).sum fun i => F i)
The theorem `padicValRat.sum_pos_of_pos` states that, given a prime number `p` and a natural number `n`, if for all natural numbers `i` less than `n`, the `p`-adic valuation of the rational numbers `F(i)` is positive, then, provided the sum of the `F(i)` for `i` in the range `0` to `n-1` is non-zero, the `p`-adic valuation of this sum will also be positive. In other words, if all the `p`-adic valuation of each element in a finite sequence of rational numbers is positive and their sum is non-zero, then the `p`-adic valuation of their sum is positive as well.
More concisely: If all the `p`-adic valuations of a finite sequence of rational numbers are positive and their sum is non-zero, then the `p`-adic valuation of their sum is positive.
|
padicValNat.mul
theorem padicValNat.mul :
∀ {p a b : ℕ} [hp : Fact p.Prime], a ≠ 0 → b ≠ 0 → padicValNat p (a * b) = padicValNat p a + padicValNat p b := by
sorry
The theorem `padicValNat.mul` states that for any prime number `p` and any natural numbers `a` and `b` that are not equal to zero, the p-adic valuation of the product of `a` and `b` is equal to the sum of the p-adic valuation of `a` and the p-adic valuation of `b`. In other words, if `p` is a prime number and `a` and `b` are non-zero natural numbers, then the largest power of `p` that divides `a*b` is equal to the sum of the largest power of `p` that divides `a` and the largest power of `p` that divides `b`.
More concisely: For any prime number `p` and non-zero natural numbers `a` and `b`, the p-adic valuation of `a * b` is equal to the sum of the p-adic valuations of `a` and `b`.
|