ProbablePrime — Mathlib

English

For every base b ≥ 1, there exist infinitely many Fermat pseudoprimes to base b.

Русский

Для каждого основания b ≥ 1 существует бесконечно много псевдо-простых чисел Фермат для основания b.

LaTeX

$$ExistsInfinitePseudoprimes\\( b \\ge 1 \\;: \\exists \\{n_i\\}, \\forall i, FermatPsp n_i b$$

Lean4

/-- `n` is a probable prime to base `b` if `n` passes the Fermat primality test; that is, `n` divides
`b ^ (n - 1) - 1`.
This definition implies that all numbers are probable primes to base 0 or 1, and that 0 and 1 are
probable primes to any base.
-/
def ProbablePrime (n b : ℕ) : Prop :=
  n ∣ b ^ (n - 1) - 1

Похожие утверждения