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₁