Nat.prime_of_mem_primeFactors
theorem Nat.prime_of_mem_primeFactors : ∀ {n p : ℕ}, p ∈ n.primeFactors → p.Prime
The theorem `Nat.prime_of_mem_primeFactors` states that for all natural numbers `n` and `p`, if `p` is a member of the prime factorization of `n`, then `p` is a prime number. Here, the prime factorization of a number `n` is a list of prime numbers such that their product is `n`. The function `Nat.Prime p` checks if `p` is a prime number, i.e., a natural number at least 2 whose only divisors are `p` and `1`.
More concisely: If a prime number `p` is a factor of natural number `n`, then `p` is a prime number.
|
Mathlib.Data.Nat.PrimeFin._auxLemma.4
theorem Mathlib.Data.Nat.PrimeFin._auxLemma.4 : ∀ {n p : ℕ}, (p ∈ n.primeFactors) = (p.Prime ∧ p ∣ n ∧ n ≠ 0) := by
sorry
The theorem `Mathlib.Data.Nat.PrimeFin._auxLemma.4` states that for any two natural numbers `n` and `p`, `p` is a part of the prime factors of `n` if and only if three conditions are met: `p` is a prime number, `p` divides `n` without leaving a remainder, and `n` is not equal to zero.
More concisely: A natural number `p` is a prime factor of another natural number `n` if and only if `p` is a prime number, `p` divides `n`, and `n` is non-zero.
|
Nat.mem_primeFactors
theorem Nat.mem_primeFactors : ∀ {n p : ℕ}, p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0
The theorem `Nat.mem_primeFactors` states that for any natural numbers `n` and `p`, `p` is a member of the prime factors of `n` if and only if `p` is a prime number, `p` divides `n`, and `n` is not equal to zero. In other words, a natural number `p` is a prime factor of another natural number `n` exactly when `p` is a prime number that divides `n`, and `n` is not zero. This theorem serves as a characterization of prime factors in terms of primality, divisibility, and non-zero conditions.
More concisely: A natural number `p` is a prime factor of another natural number `n` if and only if `p` is a prime number that divides `n` and `n` is non-zero.
|
Nat.primeFactors_mul
theorem Nat.primeFactors_mul : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (a * b).primeFactors = a.primeFactors ∪ b.primeFactors := by
sorry
This theorem states that for any two non-zero natural numbers `a` and `b`, the set of prime factors of their product `a * b` is equal to the union of the sets of prime factors of `a` and `b`. In other words, the prime factors of the product of two numbers are precisely the prime factors of the individual numbers.
More concisely: The set of prime factors of the product of two natural numbers is equal to the union of the sets of prime factors of each number.
|
Nat.infinite_setOf_prime
theorem Nat.infinite_setOf_prime : {p | p.Prime}.Infinite
The theorem `Nat.infinite_setOf_prime` states that the set of prime numbers is infinite. In other words, there are infinitely many natural numbers that are prime, where a prime number is defined as a natural number at least 2 whose only divisors are itself and 1. This theorem is a version of `Nat.exists_infinite_primes` which uses the `Set.Infinite` predicate to define infiniteness of a set.
More concisely: The set of prime natural numbers is infinite.
|
Nat.primeFactors_prime_pow
theorem Nat.primeFactors_prime_pow : ∀ {k p : ℕ}, k ≠ 0 → p.Prime → (p ^ k).primeFactors = {p}
This theorem states that for any natural numbers `p` and `k`, given that `k` is not zero and `p` is a prime number, the only prime divisor of `p` raised to the power of `k` is `p` itself. In mathematical terms, if $p$ is a prime number and $k$ is a non-zero natural number, then the set of prime factors of $p^k$ is the singleton set containing only $p$.
More concisely: For any prime number p and non-zero natural number k, the prime factorization of p^k consists only of the prime p itself.
|
Nat.dvd_of_mem_primeFactors
theorem Nat.dvd_of_mem_primeFactors : ∀ {n p : ℕ}, p ∈ n.primeFactors → p ∣ n
This theorem states that for any natural numbers `n` and `p`, if `p` is a member of the prime factors of `n`, then `p` divides `n`. In mathematical terms, for any pair of integers $(n, p)$, if $p$ is a prime factor of $n$, then there exists an integer $k$ such that $n = p \cdot k$.
More concisely: If a prime number `p` is a factor of natural number `n`, then `p` divides `n`. (Equivalently, every prime factor of `n` is a divisor of `n`.)
|