fermatPsp_base_one — Mathlib

English

All composite numbers are Fermat pseudoprimes to base 1.

Русский

Все составные числа являются псевдопростыми Фермато по основанию 1.

LaTeX

$$FermatPsp n 1 for composite n$$

Lean4

/-- All composite numbers are Fermat pseudoprimes to base 1.
-/
theorem fermatPsp_base_one {n : ℕ} (h₁ : 1 < n) (h₂ : ¬n.Prime) : FermatPsp n 1 :=
  by
  refine ⟨show n ∣ 1 ^ (n - 1) - 1 from ?_, h₂, h₁⟩
  exact show 0 = 1 ^ (n - 1) - 1 by simp ▸ dvd_zero n

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