3ac681e
1
2
3
4
5
import Mathlib theorem square_root_two_irrational (n m : ℕ) (h : n^2 = 2 * m^2) (hm : m ≠ 0) : False := by sorry
