Nat.factorization_zero
theorem Nat.factorization_zero : Nat.factorization 0 = 0
The theorem `Nat.factorization_zero` states that the factorization of zero, as defined by the `Nat.factorization` function, is equal to zero. In other words, this states that zero has no prime factors, since the factorization of a number is a function mapping each of its prime factor to its multiplicity, and for zero, this function is identically zero.
More concisely: The theorem `Nat.factorization_zero` asserts that the factorization of zero, according to the `Nat.factorization` function, is the empty map.
|
Nat.Prime.factorization_self
theorem Nat.Prime.factorization_self : ∀ {p : ℕ}, p.Prime → p.factorization p = 1
This theorem states that for any prime number `p`, the multiplicity of `p` in its own factorization is `1`. In other words, when a prime number is factored into its irreducible components (a process governed by the `factorization` function), the prime number `p` appears exactly once. This result is a basic property of prime numbers and is consistent with the definition of prime numbers in number theory.
More concisely: For any prime number `p`, the multiplicity of `p` in its own factorization is 1. (In other words, prime numbers have irreducible factorization with exactly one occurrence of `p`.)
|
Nat.factorization_eq_of_coprime_left
theorem Nat.factorization_eq_of_coprime_left :
∀ {p a b : ℕ}, a.Coprime b → p ∈ a.factors → (a * b).factorization p = a.factorization p
The theorem `Nat.factorization_eq_of_coprime_left` asserts that for any natural numbers `p`, `a`, and `b`, if `a` and `b` are coprime (i.e., their greatest common divisor is 1) and `p` is a prime factor of `a`, then the exponent of `p` in the prime factorization of `a` is the same as the exponent of `p` in the prime factorization of the product `a*b`. This statement is a property of prime factorization in the context of unique factorization domains.
More concisely: If natural numbers `a`, `b`, and `p` satisfy `gcd(a, b) = 1` and `p` is a prime factor of `a`, then the exponents of `p` in the prime factorizations of `a` and `a*b` are equal.
|
Nat.eq_iff_prime_padicValNat_eq
theorem Nat.eq_iff_prime_padicValNat_eq :
∀ (a b : ℕ), a ≠ 0 → b ≠ 0 → (a = b ↔ ∀ (p : ℕ), p.Prime → padicValNat p a = padicValNat p b)
This theorem states that two positive natural numbers, `a` and `b`, are equal if and only if their p-adic valuations are equal for every prime number `p`. This means that for every prime number `p`, the highest power of `p` that divides `a` is the same as the highest power of `p` that divides `b`. Note that `a` and `b` must be non-zero for this theorem to apply.
More concisely: Two positive natural numbers `a` and `b` are equal if and only if their p-adic valuations are equal for all primes `p`, i.e., the highest power of each prime `p` that divides `a` is equal to the highest power of `p` that divides `b`.
|
Nat.Prime.factorization_pos_of_dvd
theorem Nat.Prime.factorization_pos_of_dvd : ∀ {n p : ℕ}, p.Prime → n ≠ 0 → p ∣ n → 0 < n.factorization p
The theorem `Nat.Prime.factorization_pos_of_dvd` states that for every two natural numbers `n` and `p`, if `p` is a prime number, `n` is not zero, and `p` divides `n` (i.e., `p` is a factor of `n`), then the multiplicity of `p` in the prime factorization of `n` is greater than zero. Here, the function `Nat.factorization n` maps each prime factor of `n` to its multiplicity in `n`.
More concisely: If a prime number `p` divides a natural number `n` (`p` is a factor of `n`), then the multiplicity of `p` in the prime factorization of `n` is positive.
|
Nat.factorization_le_iff_dvd
theorem Nat.factorization_le_iff_dvd : ∀ {d n : ℕ}, d ≠ 0 → n ≠ 0 → (d.factorization ≤ n.factorization ↔ d ∣ n) := by
sorry
This theorem states that for any two non-zero natural numbers `d` and `n`, the factorization of `d` is less than or equal to the factorization of `n` if and only if `d` divides `n`. Here, the factorization of a natural number is represented by a function that maps each prime factor of the number to its multiplicity in the number. This theorem provides a connection between the divisibility of two numbers and the relationship of their prime factorizations.
More concisely: For all natural numbers d and n with d ≠ 0, d divides n if and only if the prime factorizations of d and n have the same multiplicities for each prime factor.
|
Nat.Ioc_filter_dvd_card_eq_div
theorem Nat.Ioc_filter_dvd_card_eq_div : ∀ (n p : ℕ), (Finset.filter (fun x => p ∣ x) (Finset.Ioc 0 n)).card = n / p
This theorem states that for any two natural numbers `n` and `p`, the number of natural numbers in the open interval `(0, n]` that are divisible by `p` is exactly `n / p`. This is determined by filtering the set of natural numbers in `(0, n]` to include only those that are divisible by `p`, and then counting the cardinality of this filtered set.
More concisely: The number of natural numbers in the open interval (0, n] that are divisible by p is equal to the integer division n by p.
|
Nat.card_multiples'
theorem Nat.card_multiples' :
∀ (N n : ℕ), (Finset.filter (fun k => k ≠ 0 ∧ n ∣ k) (Finset.range N.succ)).card = N / n
This theorem states that for any given non-negative integers `N` and `n`, the number of positive multiples of `n` that are less than or equal to `N` is precisely `⌊N/n⌋`. This is calculated by filtering out all the elements in the set of natural numbers from `0` to `N` (inclusive) that are divisible by `n` and not equal to `0`, and then counting the number of such elements. The theorem also suggests referring to a similar theorem, `Nat.card_multiples`, which might be a version shifted by one.
More concisely: The number of positive multiples of `n` less than or equal to `N` is equal to the integer part of `N` divided by `n`.
|
Nat.factorization_eq_zero_iff'
theorem Nat.factorization_eq_zero_iff' : ∀ (n : ℕ), n.factorization = 0 ↔ n = 0 ∨ n = 1
This theorem states that for any natural number `n`, the factorization of `n` is equal to zero if and only if `n` itself is equal to zero or one. In other words, the only natural numbers that have an empty prime factorization (i.e., no prime factors) are zero and one.
More concisely: The natural number `n` has an empty prime factorization if and only if `n` is equal to zero or one.
|
Nat.Icc_factorization_eq_pow_dvd
theorem Nat.Icc_factorization_eq_pow_dvd :
∀ (n : ℕ) {p : ℕ},
p.Prime → Finset.Icc 1 (n.factorization p) = Finset.filter (fun i => p ^ i ∣ n) (Finset.Ico 1 n)
The theorem `Nat.Icc_factorization_eq_pow_dvd` states that for any natural number `n` and a prime number `p`, the set of all positive powers of `p` that divide `n` is exactly the set of all positive natural numbers up to the value of the factorization of `n` over `p`. In other words, if you take all the positive powers of `p` that can divide `n` and put them in a set, that set will be identical to the set of positive natural numbers from 1 to the factorization of `n` over `p`, inclusive. This is represented as `Finset.Icc 1 (n.factorization p) = Finset.filter (fun i => p ^ i ∣ n) (Finset.Ico 1 n)`.
More concisely: For any natural number `n` and prime `p`, the set of positive powers of `p` dividing `n` equals the set of natural numbers from 1 to the factorization of `n` over `p`.
|
Nat.exists_eq_pow_mul_and_not_dvd
theorem Nat.exists_eq_pow_mul_and_not_dvd : ∀ {n : ℕ}, n ≠ 0 → ∀ (p : ℕ), p ≠ 1 → ∃ e n', ¬p ∣ n' ∧ n = p ^ e * n' := by
sorry
The theorem `Nat.exists_eq_pow_mul_and_not_dvd` states that given a nonzero natural number `n` and another natural number `p` which is not equal to 1, there exist natural numbers `e` and `n'` such that `n'` is not divisible by `p` and `n` is equal to `p` raised to the power `e` multiplied by `n'`.
More concisely: For any nonzero natural number `n` and prime number `p` different from 1, there exist natural numbers `e` and `n'` such that `n = p^e * n'` and `p` does not divide `n'`.
|
Nat.factorization_ord_compl
theorem Nat.factorization_ord_compl :
∀ (n p : ℕ), (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
The theorem `Nat.factorization_ord_compl` states that for all natural numbers `n` and `p`, the factorization of `n` divided by `p` raised to the power of the multiplicity of `p` in `n` (which is obtained from the factorization of `n`) equals the factorization of `n` with the multiplicity of `p` set to zero. This means we're removing the contribution of the prime `p` from the factorization of `n`. In other words, we divide `n` by as many powers of `p` as `p` appears in the factorization of `n`, and this results in a new factorization equivalent to the original one, but with the count of `p` reduced to zero.
More concisely: For all natural numbers `n` and `p`, the power of `p` in the prime factorization of `n` equals the product of `p` and the multiplicity of `p` in the prime factorization of `n` divided by the power of `p` in the prime factorization of `n`, or in other words, `p^(multiplicity p n) = n / (power p (factorization n p))`.
|
Nat.Prime.eq_of_factorization_pos
theorem Nat.Prime.eq_of_factorization_pos : ∀ {p q : ℕ}, p.Prime → p.factorization q ≠ 0 → p = q
The theorem `Nat.Prime.eq_of_factorization_pos` states that for any two natural numbers `p` and `q`, if `p` is a prime number and the factorization of `q` with respect to `p` is nonzero, then `p` must be equal to `q`. In other words, the only natural number `q` for which a prime number `p` can be a nonzero factor is `p` itself.
More concisely: If a prime number `p` is a nonzero factor of `q`, then `p = q`.
|
Nat.prod_factorization_eq_prod_primeFactors
theorem Nat.prod_factorization_eq_prod_primeFactors :
∀ {n : ℕ} {β : Type u_1} [inst : CommMonoid β] (f : ℕ → ℕ → β),
n.factorization.prod f = n.primeFactors.prod fun p => f p (n.factorization p)
The theorem `Nat.prod_factorization_eq_prod_primeFactors` states that for any natural number `n`, and any function `f` mapping two natural numbers to a type `β` that forms a commutative monoid, the product over `n.factorization` using the function `f` is equal to the product over `n.primeFactors` where for each prime factor `p`, the function `f` is applied to `p` and the count of `p` in `n.factorization`.
More concisely: For any commutative monoid homomorphism `f` and natural number `n`, the product of `n`'s prime factors using `f` is equal to the product over `n`'s factorization using `f` on each factor and its multiplicity.
|
Nat.factorization_eq_zero_of_non_prime
theorem Nat.factorization_eq_zero_of_non_prime : ∀ (n : ℕ) {p : ℕ}, ¬p.Prime → n.factorization p = 0
The theorem `Nat.factorization_eq_zero_of_non_prime` states that for any natural number `n` and any other natural number `p`, if `p` is not prime, then the factorization of `n` at `p` is equal to zero. In other words, non-prime numbers do not contribute to the prime factorization of a number.
More concisely: For any natural number `n` and non-prime natural number `p`, `n.have_factor p` implies `n = 0`.
|
Nat.factorization_mul
theorem Nat.factorization_mul :
∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (a * b).factorization = a.factorization + b.factorization
The theorem `Nat.factorization_mul` states that for any two nonzero natural numbers `a` and `b`, the factorization of the product `a * b` is equal to the sum of the factorizations of `a` and `b`. In other words, the multiplicity of a prime `p` in the prime factorization of `a * b` is the sum of the multiplicities of `p` in the prime factorizations of `a` and `b`. This accords with the fundamental theorem of arithmetic, which tells us that the primes in the factorization of `a*b` should exactly match those in `a` and `b`, simply with their multiplicities added together.
More concisely: For all nonzero natural numbers a and b, the prime factorizations of a * b are equal to the sum of the prime factorizations of a and b.
|
Nat.Prime.pow_dvd_iff_le_factorization
theorem Nat.Prime.pow_dvd_iff_le_factorization : ∀ {p k n : ℕ}, p.Prime → n ≠ 0 → (p ^ k ∣ n ↔ k ≤ n.factorization p)
This theorem states that for any natural numbers `p`, `k`, and `n`, where `p` is a prime number and `n` is not zero, `p` raised to the power of `k` divides `n` if and only if `k` is less than or equal to the multiplicity of `p` in the prime factorization of `n`. In other words, the exponent of a prime `p` in the prime factorization of `n` is at least `k` if `p^k` is a divisor of `n`.
More concisely: For a prime number `p` and natural numbers `k` and `n` with `n \neq 0`, `p^k` divides `n` if and only if the multiplicity of `p` in the prime factorization of `n` is greater than or equal to `k`.
|
Nat.Prime.factorization_pow
theorem Nat.Prime.factorization_pow : ∀ {p k : ℕ}, p.Prime → (p ^ k).factorization = fun₀ | p => k
This theorem states that for a prime number `p` and a natural number `k`, the prime factorization of `p` raised to the power of `k` only includes `p` as the prime factor with `k` as its multiplicity. In other words, if you factorize `p^k`, where `p` is a prime number, you only get `p` and it appears `k` times. This aligns with the fundamental theorem of arithmetic which states that every natural number greater than 1 has a unique prime factorization, up to the order of the factors.
More concisely: For a prime number p and a natural number k, the prime factorization of p^k consists only of p with multiplicity k.
|
Nat.prod_primeFactors_dvd
theorem Nat.prod_primeFactors_dvd : ∀ (n : ℕ), (n.primeFactors.prod fun p => p) ∣ n
The theorem `Nat.prod_primeFactors_dvd` states that for any natural number `n`, the product of its prime factors divides `n`. Here, `n.primeFactors` represents the set of prime factors of `n` and `Finset.prod` is used to compute the product of these factors. The statement is pretty much a formalized version of the fundamental theorem of arithmetic, which says that every integer greater than 1 can be uniquely written as a product of prime numbers.
More concisely: For any natural number $n$, the product of $n$'s prime factors is a divisor of $n$.
|
Nat.factorization_prod_pow_eq_self
theorem Nat.factorization_prod_pow_eq_self : ∀ {n : ℕ}, n ≠ 0 → (n.factorization.prod fun x x_1 => x ^ x_1) = n := by
sorry
This theorem states that for any non-zero natural number `n`, the product of the powers of each prime factor of `n`, where each prime factor is raised to its multiplicity in `n`, equals `n` itself. In other words, it says that if you factorize `n` into its prime factors and raise each prime factor to the power of its multiplicity in the factorization of `n`, then the product of all these terms will give you `n` back. This is essentially the fundamental theorem of arithmetic which states that every integer greater than 1 either is prime itself or is the product of prime numbers, and this product is unique, up to the order of the factors.
More concisely: For any natural number `n` > 1, `n` is the product of its prime factors raised to the powers equal to their multiplicities in `n`'s prime factorization.
|
Nat.factorization_mul_apply_of_coprime
theorem Nat.factorization_mul_apply_of_coprime :
∀ {p a b : ℕ}, a.Coprime b → (a * b).factorization p = a.factorization p + b.factorization p
This theorem states that for any three natural numbers `p`, `a`, and `b`, if `a` and `b` are coprime (i.e., their greatest common divisor is 1), then the power of `p` in the prime factorization of the product `a * b` is equal to the sum of the powers of `p` in the prime factorizations of `a` and `b` individually. In other words, if you decompose `a * b` into its prime factors, the exponent of `p` will be the same as if you had decomposed `a` and `b` individually and then added the exponents. This is a property of prime factorization in the context of unique factorization domains.
More concisely: If natural numbers `a` and `b` are coprime, then the exponent of prime `p` in the prime factorization of `a * b` is the sum of the exponents of `p` in the prime factorizations of `a` and `b`.
|
Nat.factorization_one
theorem Nat.factorization_one : Nat.factorization 1 = 0
The theorem `Nat.factorization_one` asserts that the prime factorization of the number 1 is equal to zero. In other words, the number 1 does not have any prime factors, and hence the function `Nat.factorization` when applied to 1 yields zero, indicating that there are no prime factors to count.
More concisely: The theorem asserts that the prime factorization of 1 in the natural numbers is the empty product.
|
Nat.factorization_mul_of_coprime
theorem Nat.factorization_mul_of_coprime :
∀ {a b : ℕ}, a.Coprime b → (a * b).factorization = a.factorization + b.factorization
This theorem states that for any two natural numbers, `a` and `b`, that are coprime, the factorization of the product `a * b` is equal to the sum of the factorizations of `a` and `b`. In mathematical terms, this means that if `p` is any prime number, the exponent of `p` in the prime factorization of `a * b` is the sum of the exponents of `p` in the prime factorizations of `a` and `b`. This property is tied to the fundamental theorem of arithmetic, which states that every natural number greater than 1 is either a prime number or can be written as a unique product of prime numbers, up to their order.
More concisely: If two natural numbers `a` and `b` are coprime, then the prime factorization of their product `a * b` is the concatenation of the prime factorizations of `a` and `b`.
|
Nat.support_factorization
theorem Nat.support_factorization : ∀ (n : ℕ), n.factorization.support = n.primeFactors
This theorem asserts that for any natural number `n`, the support of `n`'s factorization, i.e., the set of irreducible factors of `n` without their multiplicities, is exactly equal to `n`'s prime factors. In other words, the prime factors of `n` are precisely the distinct irreducible factors of `n` that occur in its factorization. This establishes a direct correspondence between the prime factorization of a natural number and its support in the factorization.
More concisely: The set of prime factors of a natural number equals the set of distinct irreducible factors in its factorization.
|
Nat.prod_primeFactors_prod_factorization
theorem Nat.prod_primeFactors_prod_factorization :
∀ {n : ℕ} {β : Type u_1} [inst : CommMonoid β] (f : ℕ → β),
(n.primeFactors.prod fun p => f p) = n.factorization.prod fun p x => f p
This theorem states that for any natural number `n` and a Commutative Monoid `β`, a function `f` mapping from natural numbers to `β` can transform the product over `n`'s prime factors into the product over `n`'s factorization. In other words, when the function `f` is applied to each of `n`'s prime factors and their products are taken, it yields the same result as applying `f` to each factor in `n`'s factorization and taking their products.
More concisely: For any Commutative Monoid β and natural number n, the product of applying the function f to each prime factor of n is equal to the product of applying f to each factor in n's prime factorization.
|
Nat.factorization_pow
theorem Nat.factorization_pow : ∀ (n k : ℕ), (n ^ k).factorization = k • n.factorization
This theorem states that for any natural numbers `n` and `k`, the prime factorization of `n` raised to the power of `k` is the same as `k` times the prime factorization of `n`. In other words, the multiplicity of each prime factor `p` in `n^k` is `k` times the multiplicity of `p` in `n`. This is equivalent to the mathematical statement that for any prime `p`, the power of `p` in the prime factorization of `n^k` is `k` times the power of `p` in the prime factorization of `n`.
More concisely: For any natural number `n` and `k`, the prime factorization of `n` raised to the power of `k` is `k` times the prime factorization of `n`. Equivalently, the power of each prime `p` in the prime factorization of `n^k` is `k` times its power in the prime factorization of `n`.
|
Nat.factorization_eq_of_coprime_right
theorem Nat.factorization_eq_of_coprime_right :
∀ {p a b : ℕ}, a.Coprime b → p ∈ b.factors → (a * b).factorization p = b.factorization p
The theorem `Nat.factorization_eq_of_coprime_right` states that for any three natural numbers `p`, `a`, and `b`, if `a` is coprime to `b` (i.e., the greatest common divisor of `a` and `b` is 1) and `p` is a prime factor of `b`, then the exponent of `p` in the prime factorization of `b` is the same as the exponent of `p` in the prime factorization of `a * b`. In other words, multiplying `b` by a number that is coprime to it does not change the power of any prime factor of `b` in the product's factorization.
More concisely: If `a` is coprime to `b` and `p` is a prime factor of both `a * b`, then the exponent of `p` in the prime factorization of `a * b` equals the sum of the exponents of `p` in the prime factorizations of `a` and `b`.
|
Nat.factorization_prod
theorem Nat.factorization_prod :
∀ {α : Type u_1} {S : Finset α} {g : α → ℕ},
(∀ x ∈ S, g x ≠ 0) → (S.prod g).factorization = S.sum fun x => (g x).factorization
This theorem states that for any natural number `p` and any function `g` mapping from `α` to `ℕ` that is not zero for any element in the finite set `S`, the `p`-th power in the product of `g` over the set `S` equals the sum of the `p`-th powers in `g x` for each `x` in `S`. In other words, it says that the factorization of the product of the elements in the finite set `S` under the function `g` is equal to the sum of the factorizations of each element in `S` under `g`. This extends the `factorization_mul` theorem, which is a special case when the cardinality of `S` is 2 and `g` is the identity function.
More concisely: For any finite set `S` and function `g` from a type `α` to the natural numbers not identically zero on `S`, the `p`-th power of the product of `g` over `S` equals the sum of the `p`-th powers of `g` applied to each element in `S`.
|
Nat.factorization_le_of_le_pow
theorem Nat.factorization_le_of_le_pow : ∀ {n p b : ℕ}, n ≤ p ^ b → n.factorization p ≤ b
The theorem `Nat.factorization_le_of_le_pow` states that for any natural numbers `n`, `p`, and `b`, if `n` is less than or equal to `p` raised to the power of `b`, then the exponent of `p` in the prime factorization of `n` is less than or equal to `b`. In other words, the power of any prime `p` in the prime factorization of `n` cannot exceed the highest power of `p` that divides a number not exceeding `n`. In terms of factorizations, this is saying that the count of `p` in `n`'s factorization (i.e., `n.factorization p`) is at most `b`.
More concisely: If `n` is less than or equal to `p^b`, then the exponent of `p` in the prime factorization of `n` is at most `b`.
|
Nat.prod_pow_factorization_eq_self
theorem Nat.prod_pow_factorization_eq_self :
∀ {f : ℕ →₀ ℕ}, (∀ p ∈ f.support, p.Prime) → (f.prod fun x x_1 => x ^ x_1).factorization = f
This theorem states that given a finitely supported function `f : ℕ →₀ ℕ` where the support of `f` includes only prime numbers, the factorization of the product obtained by raising each element `a` in the support of `f` to the power of `f a` results in `f` itself. In mathematical terms, if `f` is a function where every input taken from the support of `f` gives a prime number, then the factorization of the product of `a ^ f(a)` (where `a` is in the support of `f`) is equal to the original function `f`.
More concisely: For a finitely supported function `f : ℕ →₀ ℕ` with prime support, the product of `a ^ f(a)` for `a` in the support of `f` equals the function `f` itself.
|
Nat.Prime.factorization
theorem Nat.Prime.factorization : ∀ {p : ℕ}, p.Prime → p.factorization = fun₀ | p => 1
This theorem states that for any prime number `p`, the factorization of `p` only includes `p` itself with a multiplicity of `1`. In other words, in the prime factorization of a prime number, the prime number appears once and only once. This is consistent with the definition of a prime number, which has exactly two distinct natural number divisors: `1` and itself.
More concisely: A prime number `p` has a prime factorization that consists only of `p` with multiplicity 1.
|
Mathlib.Data.Nat.Factorization.Basic._auxLemma.8
theorem Mathlib.Data.Nat.Factorization.Basic._auxLemma.8 :
∀ (n p : ℕ), (n.factorization p = 0) = (¬p.Prime ∨ ¬p ∣ n ∨ n = 0)
This theorem states that for any two natural numbers `n` and `p`, the count of `p` in the prime factorization of `n` is zero if and only if `p` is not a prime number, or `p` does not divide `n`, or `n` is zero. In other words, a natural number `p` appears in the prime factorization of `n` if and only if `p` is a prime number that divides `n` and `n` is not zero.
More concisely: A natural number `p` is in the prime factorization of `n` if and only if `p` is a prime number that divides `n` and `n` is non-zero.
|
Nat.factorization_div
theorem Nat.factorization_div : ∀ {d n : ℕ}, d ∣ n → (n / d).factorization = n.factorization - d.factorization := by
sorry
The theorem `Nat.factorization_div` states that for any two natural numbers `d` and `n`, if `d` divides `n`, then the prime factorization of the quotient of `n` divided by `d` is equal to the difference of the prime factorizations of `n` and `d`. In other words, if we represent the count of prime factors as a function, the function value for `n / d` is the same as subtracting the function value for `d` from that for `n`.
More concisely: If `d` divides `n` in the natural numbers, then the prime factorizations of `n/d` and `n - d` differ only in the number of occurrences of the prime factor `d`.
|
Nat.multiplicative_factorization'
theorem Nat.multiplicative_factorization' :
∀ {n : ℕ} {β : Type u_1} [inst : CommMonoid β] (f : ℕ → β),
(∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) →
f 0 = 1 → f 1 = 1 → f n = n.factorization.prod fun p k => f (p ^ k)
This theorem states that for any natural number `n` and any type `β` that is a commutative monoid, given a multiplicative function `f` from the natural numbers to `β` that satisfies the properties `f 1 = 1` and `f 0 = 1`, and for any two natural numbers `x` and `y` that are coprime, `f (x * y) = f x * f y`. With these conditions, the function `f` evaluated at `n` is equal to the product of `f` evaluated at `p^k` for each pair `(p, k)` in the factorization of `n`. In other words, `f` can be evaluated over the factorization of `n`.
More concisely: For any commutative monoid type `β` and multiplicative function `f` from natural numbers to `β` satisfying `f 1 = 1` and `f 0 = 1`, if `x` and `y` are coprime natural numbers, then `f (x * y) = f x * f y`. Furthermore, `f n` equals the product of `f (p^k)` for all prime-power factors `(p, k)` in the prime factorization of `n`.
|
Nat.multiplicative_factorization
theorem Nat.multiplicative_factorization :
∀ {β : Type u_1} [inst : CommMonoid β] (f : ℕ → β),
(∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) →
f 1 = 1 → ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k => f (p ^ k)
The theorem `Nat.multiplicative_factorization` states that for a given multiplicative function `f` which satisfies `f 1 = 1`, and for any natural number `n` not equal to zero, the value of `f n` can be computed by evaluating `f` at `p ^ k` over the factorization of `n`. Here, `p ^ k` represents the prime factors of `n` raised to their corresponding multiplicities in `n`. This is true provided that `f` satisfies the condition that for any two numbers `x` and `y` that are coprime, `f (x * y)` equals `f x * f y`. This theorem essentially describes how a multiplicative function behaves with respect to the prime factorization of a number.
More concisely: For any multiplicative function $f$ with $f(1) = 1$ and natural number $n \neq 0$, $f(n) = \prod\_{p \mid n} f(p)^{k\_p}$, where $p$ ranges over prime factors of $n$ and $k\_p$ is their multiplicity. Given $f(x) = f(y)$ for coprime $x, y$, this expression holds.
|
Nat.ord_proj_le
theorem Nat.ord_proj_le : ∀ {n : ℕ} (p : ℕ), n ≠ 0 → p ^ n.factorization p ≤ n
This theorem establishes that for any natural number `n` that is not zero and any prime number `p`, the power of `p` raised to the multiplicity of `p` in the prime factorization of `n` is less than or equal to `n`. Here, the multiplicity of a prime factor is represented by `(Nat.factorization n) p`, which is the count of `p` in the prime factorization of `n`. In mathematical terms, if `p^k` is a term in the prime factorization of `n`, then `p^k ≤ n`.
More concisely: For any natural number $n$ and prime number $p$, the power $p^{\text{valuation}_p(n)}$ of $p$ in the prime factorization of $n$ satisfies $p^{\text{valuation}_p(n)} \leq n$.
|
Nat.card_multiples
theorem Nat.card_multiples : ∀ (n p : ℕ), (Finset.filter (fun e => p ∣ e + 1) (Finset.range n)).card = n / p
This theorem states that exactly `n / p` natural numbers in the range `[1, n]` are multiples of `p`. In other words, when you create a set of the first `n` natural numbers and then filter out only those numbers that are divisible by `p` (i.e., `p` divides `e + 1`), the cardinality (or size) of this set is `n / p`. Note that `n / p` is the integer division of `n` by `p`. This theorem provides a way to count the multiples of a given number within a specified range, using the functions `Finset.filter` and `Finset.range` in Lean 4.
More concisely: The number of natural numbers in the range [1, n] that are multiples of p is equal to the integer division n by p.
|
Nat.ord_compl_pos
theorem Nat.ord_compl_pos : ∀ {n : ℕ} (p : ℕ), n ≠ 0 → 0 < n / p ^ n.factorization p
This theorem, `Nat.ord_compl_pos`, states that for any non-zero natural number `n` and any prime number `p`, the quotient of `n` divided by `p` raised to the power of the multiplicity of `p` in the prime factorization of `n` (i.e., `p ^ (Nat.factorization n) p`) is strictly positive. In other words, after dividing `n` by the largest power of `p` that divides `n`, the result is always greater than zero.
More concisely: For any non-zero natural number `n` and prime number `p`, the quotient of `n` divided by `p` raised to the power of the multiplicity of `p` in the prime factorization of `n` is positive.
|
Nat.factorization_inj
theorem Nat.factorization_inj : Set.InjOn Nat.factorization {x | x ≠ 0}
The theorem `Nat.factorization_inj` states that the prime factorization of every nonzero natural number is unique. More formally, if we have two different nonzero natural numbers, their prime factorizations (a function mapping each prime factor to its multiplicity) can't be the same. In other words, the `Nat.factorization` function, when restricted to the set of nonzero natural numbers, is injective - it does not map two different numbers to the same prime factorization.
More concisely: The prime factorization of every non-zero natural number is unique. In other words, the function `Nat.factorization` restricting to non-zero natural numbers is injective.
|
Nat.factorization_def
theorem Nat.factorization_def : ∀ (n : ℕ) {p : ℕ}, p.Prime → n.factorization p = padicValNat p n
The theorem `Nat.factorization_def` states that for every natural number `n` and for every prime number `p`, the multiplicity of `p` in the prime factorization of `n` (given by `(Nat.factorization n) p`) is the same as the `p`-adic valuation of `n`. In other words, the `p`-adic valuation function `padicValNat p n` and the function `Nat.factorization n` mapping a prime number to its multiplicity produce the same result for any prime `p` and natural number `n`. This means that `p` appears in the prime factorization of `n` exactly as many times as `p` to some power evenly divides `n`.
More concisely: The theorem `Nat.factorization_def` asserts that for all natural numbers `n` and prime numbers `p`, the multiplicity of `p` in the prime factorization of `n` equals the `p`-adic valuation of `n`.
|
Nat.eq_of_factorization_eq
theorem Nat.eq_of_factorization_eq :
∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (∀ (p : ℕ), a.factorization p = b.factorization p) → a = b
This theorem states that for any two non-zero natural numbers `a` and `b`, if the factorization of `a` and `b`, i.e., the mappings from their prime factors to their multiplicities, are the same for every prime number `p`, then `a` and `b` must be equal. In other words, two natural numbers are equal if and only if they have the same prime factorization, which is a mathematical manifestation of the fundamental theorem of arithmetic.
More concisely: Two natural numbers are equal if and only if they have the same prime factorization.
|
Nat.factorization_lt
theorem Nat.factorization_lt : ∀ {n : ℕ} (p : ℕ), n ≠ 0 → n.factorization p < n
This theorem provides a rough upper bound on the number of times a prime `p` divides `n`, as represented by the `factorization` function. Specifically, for any natural number `n` and any prime `p`, as long as `n` is not zero, the number of times `p` appears in the factorization of `n` is strictly less than `n`.
More concisely: For any prime number p and natural number n neither equal to zero, the number of occurrences of p in the prime factorization of n is strictly less than n.
|
Nat.eq_pow_of_factorization_eq_single
theorem Nat.eq_pow_of_factorization_eq_single : ∀ {n p k : ℕ}, n ≠ 0 → (n.factorization = fun₀ | p => k) → n = p ^ k
This theorem states that given three natural numbers `n`, `p`, and `k`, where `n` is not equal to zero, if the factorization of `n` contains just one number `p` (with multiplicity `k`), then `n` can be expressed as `p` raised to the power `k`. In other words, `n` is a power of `p`.
More concisely: If natural number `n` is not zero and its prime factorization contains a prime number `p` with multiplicity `k`, then `n = p^k`.
|
Nat.ord_proj_dvd
theorem Nat.ord_proj_dvd : ∀ (n p : ℕ), p ^ n.factorization p ∣ n
The theorem `Nat.ord_proj_dvd` states that for any two natural numbers `n` and `p`, the power of `p` to the value given by the function `Nat.factorization` applied to `n` and `p` divides `n`. In terms of mathematics, this means that for any pair of natural numbers (n, p), the power of p to the multiplicity of p in the prime factorization of n (i.e., the number of times p appears as a factor in the prime factorization of n) divides n.
More concisely: For all natural numbers n and p, the p-th power of the multiplicity of p in the prime factorization of n divides n.
|
Nat.factors_count_eq
theorem Nat.factors_count_eq : ∀ {n p : ℕ}, List.count p n.factors = n.factorization p
The theorem `Nat.factors_count_eq` states that for any natural numbers `n` and `p`, the count of `p` in the list of prime factors of `n` (given by `List.count p (Nat.factors n)`) is equal to the multiplicity of `p` in the prime factorization of `n` (given by `(Nat.factorization n) p`). In other words, both expressions represent the exponent of prime `p` in the prime factorization of `n`, and the theorem declares the latter expression as the standard or simplified form.
More concisely: The number of occurrences of prime number `p` in the prime factorization of natural number `n` (given by `Nat.factorization n p`) equals the count of `p` in the list of prime factors of `n` (given by `List.count p (Nat.factors n)`).
|