We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent ba141eb commit 738c3c4Copy full SHA for 738c3c4
FLT.lean
@@ -20,3 +20,4 @@ theorem PNat.pow_add_pow_ne_pow
20
(n : ℕ) (hn : n > 2) :
21
x^n + y^n ≠ z^n :=
22
PNat.pow_add_pow_ne_pow_of_FermatLastTheorem FLT.Wiles_Taylor_Wiles x y z n hn
23
+
0 commit comments