Square_Root_of_Prime_is_Irrational
Provedirrationality-proofsprime-numbersproofwikisquare-root-of-prime-is-irrationalsquare-roots
The square root of any prime number is irrational.
Preamble
import Mathlib.Data.Real.Irrational import Mathlib.Data.Nat.Prime.Basic import Mathlib.Tactic
Formal statement
theorem Square_Root_of_Prime_is_Irrational (p : ℕ) (hp : Nat.Prime p) : Irrational (Real.sqrt p) := by sorry
Source