Nat.mem_factors
theorem Nat.mem_factors : ∀ {n p : ℕ}, n ≠ 0 → (p ∈ n.factors ↔ p.Prime ∧ p ∣ n)
The theorem `Nat.mem_factors` states that for all natural numbers `n` and `p`, given that `n` is not equal to zero, `p` is a member of the list of prime factors of `n` if and only if `p` is a prime number and `p` divides `n`. Here, `Nat.Prime p` means `p` is a prime number, meaning it is a natural number greater than or equal to 2 whose only divisors are `p` and `1`, and `p ∣ n` means `p` divides `n`.
More concisely: For a prime number `p` to be a factor of a natural number `n` (i.e., `p | n`), it must be a prime factor of `n` (belong to the list of prime factors of `n`).
|
Nat.factors_one
theorem Nat.factors_one : Nat.factors 1 = []
The theorem `Nat.factors_one` states that the prime factorization of 1 is an empty list. In other words, the number 1 does not have any prime factors.
More concisely: The theorem `Nat.factors_one` asserts that the prime factorization of 1 is the empty list.
|
Nat.mem_factors_mul_left
theorem Nat.mem_factors_mul_left : ∀ {p a b : ℕ}, p ∈ a.factors → b ≠ 0 → p ∈ (a * b).factors
This theorem states that if `p` is a prime factor of a natural number `a`, then `p` is also a prime factor of the product of `a` and any other natural number `b` that is not zero. In other words, a prime factor of a number remains a prime factor when that number is multiplied by any non-zero natural number.
More concisely: If `p` is a prime factor of natural number `a`, then `p` is a prime factor of the product `a * b` for any non-zero natural number `b`.
|
Nat.coprime_factors_disjoint
theorem Nat.coprime_factors_disjoint : ∀ {a b : ℕ}, a.Coprime b → a.factors.Disjoint b.factors
This theorem states that for any two natural numbers `a` and `b` that are coprime (i.e., their greatest common divisor is 1), the sets of their factors are disjoint. In other words, there is no common factor between `a` and `b` except for 1. This implies that any factor of `a` or `b` is less than or equal to 1, which is considered as the bottom element in the lattice structure of natural numbers under the order of "less than or equal to".
More concisely: For coprime natural numbers `a` and `b`, their sets of factors are disjoint, meaning there is no common factor except for 1.
|
Nat.factors_unique
theorem Nat.factors_unique : ∀ {n : ℕ} {l : List ℕ}, l.prod = n → (∀ p ∈ l, p.Prime) → l.Perm n.factors
The theorem `Nat.factors_unique` represents the Fundamental Theorem of Arithmetic. It states that for any natural number `n` and any list of natural numbers `l`, if the product of the elements in `l` equals `n` and each number `p` in `l` is prime, then `l` is a permutation of the prime factorization of `n`. In other words, every natural number has a unique prime factorization (up to the order of the factors).
More concisely: Every natural number has a unique prime factorization.
|
Nat.mem_factors_mul
theorem Nat.mem_factors_mul :
∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → ∀ {p : ℕ}, p ∈ (a * b).factors ↔ p ∈ a.factors ∨ p ∈ b.factors
The theorem `Nat.mem_factors_mul` states that for any two natural numbers `a` and `b`, if neither `a` nor `b` are zero, then a natural number `p` is in the prime factorization of the product `a * b` if and only if `p` is in the prime factorization of `a` or `p` is in the prime factorization of `b`. This expresses that the prime factors of a product of two non-zero numbers are exactly the union of the prime factors of the individual numbers.
More concisely: The prime factors of the product of two non-zero natural numbers are the same as the union of their prime factor sets.
|
Nat.pos_of_mem_factors
theorem Nat.pos_of_mem_factors : ∀ {n p : ℕ}, p ∈ n.factors → 0 < p
This theorem states that for any natural numbers `n` and `p`, if `p` is an element of the prime factorization of `n` (denoted as `Nat.factors n`), then `p` is greater than zero. In other words, every prime factor of a natural number is positive.
More concisely: Every prime factor of a natural number is a positive number.
|
Nat.dvd_of_mem_factors
theorem Nat.dvd_of_mem_factors : ∀ {n p : ℕ}, p ∈ n.factors → p ∣ n
The theorem `Nat.dvd_of_mem_factors` states that for any two natural numbers `n` and `p`, if `p` is an element in the prime factorization of `n` (as defined by `Nat.factors n`), then `p` divides `n`. In more mathematical terms, if $p$ is a prime factor of $n$, then $n$ is divisible by $p$. This is a key property of prime factorization, asserting that all the factors listed indeed divide the original number.
More concisely: If a prime number `p` is in the factorization of a natural number `n` (as defined by `Nat.factors n`), then `n` is divisible by `p`.
|
Nat.perm_factors_mul
theorem Nat.perm_factors_mul : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (a * b).factors.Perm (a.factors ++ b.factors)
This theorem states that for any two positive numbers `a` and `b`, the prime factorization of their product `a * b` is a permutation of the concatenation of the prime factorizations of `a` and `b`. That is, the prime factors of `a * b` are exactly the collection of the prime factors of `a` and `b`, possibly rearranged.
More concisely: The product of two positive numbers has the same prime factors, possibly in a different order, as the concatenation of their prime factorizations.
|
Nat.mem_factors_iff_dvd
theorem Nat.mem_factors_iff_dvd : ∀ {n p : ℕ}, n ≠ 0 → p.Prime → (p ∈ n.factors ↔ p ∣ n)
The theorem `Nat.mem_factors_iff_dvd` states that for any two distinct natural numbers `n` and `p`, where `n` is not equal to zero and `p` is a prime number, `p` is a factor of `n` (expressed as `p ∈ Nat.factors n`) if and only if `p` divides `n` (expressed as `p ∣ n`). This theorem is essentially saying that a prime number `p` is included in the prime factorization list of a non-zero natural number `n` if and only if `p` is a divisor of `n`.
More concisely: A prime number `p` divides natural number `n` if and only if `p` is a factor in the prime factorization of `n`.
|
Nat.Prime.factors_pow
theorem Nat.Prime.factors_pow : ∀ {p : ℕ}, p.Prime → ∀ (n : ℕ), (p ^ n).factors = List.replicate n p
The theorem `Nat.Prime.factors_pow` states that for any natural number `p` which is a prime number, for all natural number `n`, the prime factorization of `p` raised to the power `n` is a list composed of `n` copies of `p`. In other words, if `p` is a prime number, then the prime factorization of `p^n` always consists of `p` repeated `n` times.
More concisely: For any prime number p and natural number n, the prime factorization of p^n is a list of n copies of p. (Equivalently, the prime factorization of p raised to the power n is p^n.)
|
Nat.factors_zero
theorem Nat.factors_zero : Nat.factors 0 = []
The theorem `Nat.factors_zero` states that the prime factorization of zero is an empty list. This is because zero is not considered to have any prime factors in the context of this prime factorization function.
More concisely: The prime factorization of zero is the empty list.
|
Nat.perm_factors_mul_of_coprime
theorem Nat.perm_factors_mul_of_coprime : ∀ {a b : ℕ}, a.Coprime b → (a * b).factors.Perm (a.factors ++ b.factors) := by
sorry
This theorem states that for any two coprime natural numbers `a` and `b`, the prime factors of the product `a * b` are the same as the combination of the prime factors of `a` and `b`. In other words, the list of prime factors of `a * b` is a permutation of the list obtained by concatenating the prime factors of `a` and `b`. This is true under the condition that `a` and `b` are coprime, which means they do not have any common prime factors.
More concisely: For coprime natural numbers `a` and `b`, the prime factorization of their product `a * b` is the concatenation of their prime factorizations.
|
Nat.prod_factors
theorem Nat.prod_factors : ∀ {n : ℕ}, n ≠ 0 → n.factors.prod = n
The theorem `Nat.prod_factors` in Lean 4 asserts that for every natural number `n` such that `n` is not equal to zero, the product of the list of its prime factors (as given by the function `Nat.factors n`) equals the number `n` itself. In other words, if you take a non-zero natural number, find all its prime factors, and multiply them together, you get the original number back. This is a formalization of the fundamental theorem of arithmetic, which states that every integer greater than 1 either is a prime number itself or can be factored as a product of primes in an essentially unique way.
More concisely: For every natural number `n` greater than zero, `n` is the product of its prime factors.
|
Nat.mem_factors_mul_right
theorem Nat.mem_factors_mul_right : ∀ {p a b : ℕ}, p ∈ b.factors → a ≠ 0 → p ∈ (a * b).factors
The theorem `Nat.mem_factors_mul_right` states that for any natural numbers `p`, `a` and `b` if `p` is a prime factor of `b`, `a` is non-zero, then `p` is also a prime factor of the product `a * b`. Essentially, it means multiplying a number (other than zero) with another number does not eliminate any of the prime factors of the latter number.
More concisely: If a prime number p divides b, then p also divides the product a * b for any non-zero natural number a.
|
Nat.factors_add_two
theorem Nat.factors_add_two : ∀ (n : ℕ), (n + 2).factors = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).factors := by
sorry
This theorem states that the list of prime factors of any natural number `n + 2` can be constructed through an inductive process. The process begins by taking the smallest prime factor (`minFac`) of `n + 2`, and then appending the prime factors of `n + 2` divided by this smallest prime factor. In other words, for any natural number `n`, the prime factorization of `n + 2` is equivalent to the smallest prime factor of `n + 2` prepended to the prime factorization of the quotient of `n + 2` and its smallest prime factor.
More concisely: The prime factorization of `n + 2` is obtained by appending the smallest prime factor of `n + 2` to the prime factorization of `(n + 2) / (prf n+2)`, where `prf n+2` is the smallest prime factor of `n + 2`.
|
Nat.factors_prime
theorem Nat.factors_prime : ∀ {p : ℕ}, p.Prime → p.factors = [p]
The theorem `Nat.factors_prime` states that for any natural number `p`, if `p` is prime, then the prime factorization of `p` is just the list containing `p` itself. In other words, for a prime number `p`, the only prime factor is `p`.
More concisely: For any prime number `p`, its prime factorization is the list `[p]`.
|
Nat.prime_of_mem_factors
theorem Nat.prime_of_mem_factors : ∀ {n p : ℕ}, p ∈ n.factors → p.Prime
The theorem `Nat.prime_of_mem_factors` states that for any natural numbers `n` and `p`, if `p` is an element in the factorization of `n` (`p` is a factor of `n`), then `p` is a prime number. In other words, all factors of a number `n` obtained using the function `Nat.factors` are prime numbers.
More concisely: For any natural number `n` and its factor `p`, if `p` is in the factorization of `n` (i.e., `p` divides `n`), then `p` is a prime number.
|