coprime_of_fermatPsp — Mathlib

English

If n is a FermatPsp to base b, then n is coprime with b when b ≥ 1.

Русский

Если n является псевдопростым Фермато по основанию b, то gcd(n,b)=1 при b ≥ 1.

LaTeX

$$Nat.Coprime n b$$

Lean4

/-- If `n` is a Fermat pseudoprime to base `b`, then `n` is coprime with `b`, assuming that `b` is
positive.

This lemma is a small wrapper based on `coprime_of_probablePrime`
-/
theorem coprime_of_fermatPsp {n b : ℕ} (h : FermatPsp n b) (h₁ : 1 ≤ b) : Nat.Coprime n b :=
  by
  rcases h with ⟨hp, _, hn₂⟩
  exact coprime_of_probablePrime hp (by cutsat) h₁

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