frequently_atTop_fermatPsp — Mathlib

English

There are frequently Fermat pseudoprimes to base b at arbitrarily large values.

Русский

Существует часто встречающееся псевдопростое Фермато по основанию b на больших значениях.

LaTeX

$$FrequentlyAtTop(n => FermatPsp n b)$$

Lean4

theorem frequently_atTop_fermatPsp {b : ℕ} (h : 1 ≤ b) : ∃ᶠ n in Filter.atTop, FermatPsp n b := by
  -- Based on the proof of `Nat.frequently_atTop_modEq_one`

  refine Filter.frequently_atTop.2 fun n => ?_
  obtain ⟨p, hp⟩ := exists_infinite_pseudoprimes h n
  exact ⟨p, hp.2, hp.1⟩

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