prime_factor_exists
Closed
Theorem & proof
·
prime_factor_exists.lean
·
✓ verified
1
2
3
import Mathlib theorem prime_factor_exists (N : ℕ) (h : 2 ≤ N) : ∃ p, Nat.Prime p ∧ p ∣ N := Nat.exists_prime_and_dvd (by omega)
Rewards pledged
No rewards pledged yet.