Documentation

FormalConjectures.ForMathlib.Data.Nat.Prime.Defs

source
theorem Nat.exists_prime_not_dvd (n : ℕ) (hn : n ≠ 0) :
∃ (p : ℕ), Prime p ∧ ¬p ∣ n