lean_workbook_plus_32551
Provedprove that is an irrational number.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_32551 : ¬ ∃ a b : ℕ, (a : ℝ) / b = Real.sqrt 2 := by sorry
Source
prove that is an irrational number.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_32551 : ¬ ∃ a b : ℕ, (a : ℝ) / b = Real.sqrt 2 := by sorry