test_sqrt2_irr
Provedproofwikitest
test
Preamble
import Mathlib.Data.Real.Sqrt import Mathlib.Data.Set.Basic def Irrational (x : ℝ) : Prop := x ∉ Set.range ((↑) : ℚ → ℝ)
Formal statement
theorem test_sqrt2_irr : Irrational (Real.sqrt 2) := by sorry
test
import Mathlib.Data.Real.Sqrt import Mathlib.Data.Set.Basic def Irrational (x : ℝ) : Prop := x ∉ Set.range ((↑) : ℚ → ℝ)
theorem test_sqrt2_irr : Irrational (Real.sqrt 2) := by sorry