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

State before:
x : ℝ
⊢ irrational x ↔ ∀ (a b : ℤ), x ≠ ↑a / ↑b
Tactic:
sorry
State after:
no goals