Theorems · Theorem · number theory

Nat.exists_infinite_pseudoprimes

∀ {b : ℕ}, 1 ≤ b → ∀ (m : ℕ), ∃ n, n.FermatPsp b ∧ m ≤ n

For all positive bases, there exist infinitely many Fermat pseudoprimes to that base. Given in this form: for all numbers b ≥ 1 and m, there exists a pseudoprime n to base b such that m ≤ n. This form is similar to Nat.exists_infinite_primes.

Defined in

Mathlib.NumberTheory.FermatPsp

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound