Theorem: book.irrational.Theorem_2 (FormalBook/Chapter_08.lean)

State before:
π : ℝ
r : ℚ
h_r : r ≠ 0
⊢ irrational (π ^ 2)
Tactic:
sorry
State after:
no goals