Nat.fermatPsp_base_one
theorem Nat.fermatPsp_base_one : ∀ {n : ℕ}, 1 < n → ¬n.Prime → n.FermatPsp 1
This theorem states that all composite natural numbers are Fermat pseudoprimes to base 1. In other words, for any natural number `n` that is greater than 1 and not a prime, the statement `n.FermatPsp 1` holds true. Here, `n.FermatPsp 1` refers to the property of `n` being a Fermat pseudoprime to base 1, which is a concept in number theory related to the pseudoprimality tests.
More concisely: For any composite natural number `n` greater than 1, it is a Fermat pseudoprime to base 1.
|
Nat.coprime_of_fermatPsp
theorem Nat.coprime_of_fermatPsp : ∀ {n b : ℕ}, n.FermatPsp b → 1 ≤ b → n.Coprime b
The theorem `Nat.coprime_of_fermatPsp` states that for any natural numbers `n` and `b`, if `n` is a Fermat pseudoprime to base `b`, and if `b` is greater than or equal to 1, then `n` and `b` are coprime. In mathematical terms, this means that the greatest common divisor of `n` and `b` is 1. This theorem is a derived result using the property `coprime_of_probablePrime`.
More concisely: If a natural number `n` is a Fermat pseudoprime to base `b` (where `b` is greater than or equal to 1), then `gcd(n, b) = 1`.
|
Nat.coprime_of_probablePrime
theorem Nat.coprime_of_probablePrime : ∀ {n b : ℕ}, n.ProbablePrime b → 1 ≤ n → 1 ≤ b → n.Coprime b
This theorem states that if a positive integer `n` passes the Fermat primality test to base `b`, then `n` is coprime with `b`, under the assumption that both `n` and `b` are greater than or equal to 1. In mathematical terms, being "coprime" means that the greatest common divisor (gcd) of `n` and `b` is `1`. The Fermat primality test is a probabilistic method used to determine whether a number is likely prime.
More concisely: If a positive integer `n` passes the Fermat primality test to base `b`, then `gcd(n, b) = 1`.
|
Nat.infinite_setOf_pseudoprimes
theorem Nat.infinite_setOf_pseudoprimes : ∀ {b : ℕ}, 1 ≤ b → {n | n.FermatPsp b}.Infinite
This theorem states that for any natural number `b` that is greater than or equal to 1, the set of natural numbers `n` that are Fermat pseudoprimes to the base `b` is infinite. In other words, there are infinitely many natural numbers `n` that satisfy Fermat's Little Theorem for a specific `b`, but are not actually prime numbers.
More concisely: The set of natural numbers that are Fermat pseudoprimes to base `b` for some `b` greater than or equal to 1 is infinite.
|
Nat.exists_infinite_pseudoprimes
theorem Nat.exists_infinite_pseudoprimes : ∀ {b : ℕ}, 1 ≤ b → ∀ (m : ℕ), ∃ n, n.FermatPsp b ∧ m ≤ n
This theorem states that for all positive base numbers greater than or equal to one, there exist infinite Fermat pseudoprimes to that base. More specifically, for any given numbers `b` and `m`, where `b` is greater than or equal to 1, there exists a Fermat pseudoprime `n` to the base `b` such that `n` is greater than or equal to `m`. The structure of this theorem is analogous to the theorem `Nat.exists_infinite_primes`, which asserts the existence of infinite prime numbers.
More concisely: For every positive integer `b` and `m`, there exists an infinite sequence of Fermat pseudoprimes `n` to the base `b` such that `n` is greater than or equal to `m`.
|