fixture_inf_primes
Closed
Theorem & proof
·
fixture_inf_primes.lean
·
✓ verified
1
2
3
import Mathlib theorem fixture_inf_primes (n : ℕ) : ∃ p, n < p ∧ Nat.Prime p := Nat.exists_infinite_primes n.succ
Rewards pledged
No rewards pledged yet.