Nat.multiplicity_eq_card_pow_dvd
theorem Nat.multiplicity_eq_card_pow_dvd :
∀ {m n b : ℕ},
m ≠ 1 → 0 < n → m.log n < b → multiplicity m n = ↑(Finset.filter (fun i => m ^ i ∣ n) (Finset.Ico 1 b)).card
The theorem `Nat.multiplicity_eq_card_pow_dvd` states that for any natural numbers `m`, `n`, and `b`, with `m` not equal to 1 and `n` greater than 0, if the base `m` logarithm of `n` is less than `b`, then the multiplicity of `m` in `n` is equal to the cardinality of a set. This set is given by the positive natural numbers `i` within the interval from 1 to `b` (exclusive of `b`), for which `m` raised to the power of `i` divides `n`. In other words, the multiplicity is the count of such powers of `m` that divide `n`.
More concisely: For natural numbers $m \neq 1$, $n > 0$, and $b$, if $\log_m n < b$, then the multiplicity of $m$ in $n$ equals the cardinality of the set of $i \in \mathbb{N}$ such that $i < b$ and $m^i \mid n$.
|
Nat.Prime.sub_one_mul_multiplicity_factorial
theorem Nat.Prime.sub_one_mul_multiplicity_factorial :
∀ {n p : ℕ} (hp : p.Prime), (p - 1) * (multiplicity p n.factorial).get ⋯ = n - (p.digits n).sum
The theorem `Nat.Prime.sub_one_mul_multiplicity_factorial` states that for a prime number `p`, the product of `(p - 1)` and the highest power of `p` that divides `n!` (or the multiplicity of `p` in `n!`) is equal to `n` minus the sum of the digits of `n` when represented in base `p`. This theorem connects number theory, combinatorics, and arithmetic in a subtle way. It is important to note that the multiplicity function returns the highest power of `p` that divides `n!`, not the number of times `p` divides `n!`.
More concisely: For a prime number `p`, the product of `(p - 1)` and the multiplicity of `p` in `n!` equals `n` minus the sum of the digits of `n` when represented in base `p`.
|
Nat.Prime.multiplicity_choose
theorem Nat.Prime.multiplicity_choose :
∀ {p n k b : ℕ},
p.Prime →
k ≤ n →
p.log n < b →
multiplicity p (n.choose k) =
↑(Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)).card
This theorem states that for any prime number `p` and non-negative integers `n`, `k`, and `b`, if `k` is less than or equal to `n` and the base `p` logarithm of `n` is less than `b`, then the multiplicity of `p` in the binomial coefficient "n choose k" equals the cardinality of the set of integers `i` from `1` to `b-1` such that `p^i` is less than or equal to the sum of the remainder of `k` divided by `p^i` and the remainder of `(n-k)` divided by `p^i`. In other words, the multiplicity of a prime `p` in "n choose k" is the number of carries when `k` and `(n-k)` are added in the base `p` representation. This set of integers `i` is expressed by filtering the set of all integers from `1` to `b-1`.
More concisely: The multiplicity of a prime `p` in the binomial coefficient "n choose k" equals the number of integers i from 1 to b-1 such that p^i is less than or equal to the sum of the remainders of k and (n-k) when divided by p^i in base p representation.
|
Nat.Prime.multiplicity_choose'
theorem Nat.Prime.multiplicity_choose' :
∀ {p n k b : ℕ},
p.Prime →
p.log (n + k) < b →
multiplicity p ((n + k).choose k) =
↑(Finset.filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Finset.Ico 1 b)).card
The theorem `Nat.Prime.multiplicity_choose'` states that for any prime number `p` and natural numbers `n`, `k`, and `b`, where `b` is a bound greater than the base `p` logarithm of `n + k`, the multiplicity of `p` in the binomial coefficient `choose (n + k) k` equals the number of elements in the finite set of numbers between `1` and `b` (exclusive) such that `p ^ i` is less than or equal to the sum of the base `p` residues of `k` and `n` at the `i`-th place. In other words, the multiplicity of `p` in `choose (n + k) k` corresponds to the number of carry operations when `k` and `n` are added in base `p`.
More concisely: The multiplicity of a prime number `p` in the binomial coefficient `choose (n + k) k` is equal to the number of times `p` appears as a carry during the addition of `n` and `k` in base `p`, up to a bound where `p ^ i` is less than or equal to the sum of their base `p` residues.
|
Nat.Prime.multiplicity_factorial_mul_succ
theorem Nat.Prime.multiplicity_factorial_mul_succ :
∀ {n p : ℕ},
p.Prime →
multiplicity p (p * (n + 1)).factorial = multiplicity p (p * n).factorial + multiplicity p (n + 1) + 1
For any prime number `p` and natural number `n`, the multiplicity of `p` in the factorial of `(p * (n + 1))` is one more than the sum of the multiplicities of `p` in the factorial of `(p * n)` and `n + 1`. In other words, the number of times `p` divides evenly into `(p * (n + 1))!` is equal to the number of times `p` divides evenly into `(p * n)!`, the number of times `p` divides into `n + 1`, plus one. This theorem provides a relationship between the factorizations of factorials and natural numbers in the context of prime numbers.
More concisely: For any prime number p and natural number n, the multiplicity of p in the factorial (p * (n + 1))! is one plus the multiplicity of p in the factorial (p * n)!.
|
Nat.Prime.pow_dvd_factorial_iff
theorem Nat.Prime.pow_dvd_factorial_iff :
∀ {p n r b : ℕ}, p.Prime → p.log n < b → (p ^ r ∣ n.factorial ↔ r ≤ (Finset.Ico 1 b).sum fun i => n / p ^ i) := by
sorry
The theorem states that for any natural numbers `p`, `n`, `r`, and `b`, if `p` is prime and the logarithm base `p` of `n` is less than `b`, then `p` raised to the power of `r` divides the factorial of `n` if and only if `r` is less than or equal to the sum of the quotients of `n` divided by `p` raised to the power of `i` where `i` is an element of the set of natural numbers which are greater than or equal to `1` and less than `b`. In mathematical terms, for a prime number p and natural numbers n, r, and b, if log_p(n) < b, then p^r divides n! if and only if r ≤ ∑(n/p^i) for all i in the interval [1, b).
More concisely: For a prime number p and natural numbers n, r, and b, if the logarithm base p of n is less than b, then p raises to the power of r divides the factorial of n if and only if r is less than or equal to the sum of the quotients n divided by p raised to the power of i for all i in the range [1, b).
|
Nat.Prime.multiplicity_le_multiplicity_choose_add
theorem Nat.Prime.multiplicity_le_multiplicity_choose_add :
∀ {p : ℕ}, p.Prime → ∀ (n k : ℕ), multiplicity p n ≤ multiplicity p (n.choose k) + multiplicity p k
This theorem is stating a lower bound on the multiplicity of a prime number `p` in `n choose k`. For each prime number `p`, and for all natural numbers `n` and `k`, the multiplicity of `p` in `n` is less than or equal to the sum of the multiplicity of `p` in `n choose k` and the multiplicity of `p` in `k`. The multiplicity of a number `a` in `b` is the largest natural number `n` such that `a^n` divides `b`.
More concisely: For all prime numbers p, natural numbers n, and k, the multiplicity of p dividing n choose k is less than or equal to the sum of the multiplicity of p dividing n and the multiplicity of p dividing k.
|
Nat.Prime.multiplicity_factorial
theorem Nat.Prime.multiplicity_factorial :
∀ {p : ℕ},
p.Prime → ∀ {n b : ℕ}, p.log n < b → multiplicity p n.factorial = ↑((Finset.Ico 1 b).sum fun i => n / p ^ i)
**Legendre's Theorem**
For any prime number `p` and natural numbers `n` and `b`, where the logarithm of `n` in base `p` is less than `b`, the highest power of `p` that divides `n!` (the factorial of `n`) is equal to the sum of the quotients of `n` divided by `p` to the power `i`, where `i` ranges over the elements of the set of natural numbers between `1` and `b` (exclusive). Here `b` is any bound greater than `log p n`.
More concisely: For any prime number `p` and natural numbers `n` and `b` with `log_p n < b`, the highest power of `p` dividing `n!` equals the sum of the quotients `\frac{n}{p^i}` for `i` in the range `1` to `b`.
|
Nat.Prime.multiplicity_factorial_mul
theorem Nat.Prime.multiplicity_factorial_mul :
∀ {n p : ℕ}, p.Prime → multiplicity p (p * n).factorial = multiplicity p n.factorial + ↑n
This theorem states that for any natural numbers `n` and `p`, if `p` is a prime number, then the multiplicity of `p` in the factorial of `p * n` is equal to the multiplicity of `p` in the factorial of `n` plus `n`. Here, the multiplicity of `p` in a number is the highest power of `p` that divides the number. In other words, it counts the number of times `p` appears in the prime factorization of the number. So, this theorem means that if you multiply `n` by a prime number `p` and then take the factorial, the prime `p` will appear `n` more times in the prime factorization than if you just took the factorial of `n`.
More concisely: For any natural number `n` and prime number `p`, the multiplicity of `p` in the factorial of `p * n` is one more than the multiplicity of `p` in the factorial of `n`.
|