Euclids_Lemma_for_Primes
ProvedFor any prime p, sqrt(p) is irrational. This follows from the proof by contradiction using Euclid's Lemma: if sqrt(p) = a/b in lowest terms, then p|a^2, by Euclid's Lemma p|a, contradicting lowest terms.
Preamble
import Mathlib.NumberTheory.Real.Irrational import Mathlib.Tactic
Formal statement
theorem Euclids_Lemma_for_Primes (p : ℕ) (hp : Nat.Prime p) : Irrational (Real.sqrt p) := by sorry