Theorem Details
import Mathlib
theorem pi_transcendental (p : Polynomial ℝ) (hp : (∀ n : ℕ, ∃ q : ℚ, p.coeff n = (q : ℝ))) : p.eval Real.pi ≠ 0 := sorry
Bounty: 0.0017 ETH
Status: Open