factoredNumbers_coprime — Mathlib

English

If p is prime and p ∉ s and n ∈ factoredNumbers(s), then p and n are coprime.

Русский

Если p простое и p ∉ s, и n ∈ factoredNumbers(s), то p и n взаимно просты.

LaTeX

$$Nat.Coprime p n$$

Lean4

/-- If `p ∉ s` is a prime and `n` is `s`-factored, then `p` and `n` are coprime. -/
theorem factoredNumbers_coprime {s : Finset ℕ} {p n : ℕ} (hp : p.Prime) (hs : p ∉ s) (hn : n ∈ factoredNumbers s) :
    Nat.Coprime p n := by
  rw [hp.coprime_iff_not_dvd, ← mem_primeFactorsList_iff_dvd hn.1 hp]
  exact fun H ↦ hs <| hn.2 p H

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