mathlib

c0439b48 - feat(number_theory): prove the existence of infinitely many Fermat pseudoprimes to any base (#17632)

feat(number_theory): prove the existence of infinitely many Fermat pseudoprimes to any base (#17632) A natural number `n` is a probable prime to base `b` if `n` divides `b ^ (n - 1) - 1`. `n` is a Fermat pseudoprime to base `b` if it is a composite probable prime. This commit defines Fermat pseudoprimes and proves that for any positive base `b`, there exist an infinite number of Fermat pseudoprimes to that base. Co-authored-by: Niels Voss <nvosscode@gmail.com>