infinite_setOf_pseudoprimes — Mathlib

English

For every natural number b with b ≥ 1 there are infinitely many natural numbers n such that n is a Fermat pseudoprime to base b.

Русский

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

LaTeX

$$$\\forall b \\in \\mathbb{N},\\; b \\ge 1 \\Rightarrow \\{n \\in \\mathbb{N} \\mid \\mathrm{FermatPsp}(n,b)\\} \\text{ is infinite}$$$

Lean4

/-- Infinite set variant of `Nat.exists_infinite_pseudoprimes`
-/
theorem infinite_setOf_pseudoprimes {b : ℕ} (h : 1 ≤ b) : Set.Infinite {n : ℕ | FermatPsp n b} :=
  Nat.frequently_atTop_iff_infinite.mp (frequently_atTop_fermatPsp h)

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