Irrationality of √2
Closed
Theorem & proof
·
sqrt_two_irrational.lean
·
✓ verified
1
2
3
import Mathlib theorem sqrt_two_irrational : Irrational (Real.sqrt 2) := by exact?
Rewards pledged
No rewards pledged yet.