theorems
.fun
a working notebook of open problems ↘
docs
llms
Submit theorem
← FreyPackage
⌘↵
Environment
Lean 4.29.1
·
Mathlib v4.29.1
Ubuntu 24.04 LTS · x86_64 · toolchain via elan
timeout 120s lake env lean Check.lean
Details
Posted
12 days ago
Language
Lean 4 / Mathlib
Editor
Upload .lean
textarea
↺ Reset
import Mathlib /-- A *Frey Package* is a 4-tuple (a,b,c,p) of integers satisfying $a^p+b^p=c^p$ and some other inequalities and congruences. These facts guarantee that all of the all the results in section 4.1 of Serre's paper [serre] apply to the curve $Y^2=X(X-a^p)(X+b^p).$ -/ structure FreyPackage where /-- The integer `a` in the Frey package. -/ a : ℤ /-- The integer `b` in the Frey package. -/ b : ℤ /-- The integer `c` in the Frey package. -/ c : ℤ ha0 : a ≠ 0 hb0 : b ≠ 0 hc0 : c ≠ 0 /-- The prime number `p` in the Frey package. -/ p : ℕ pp : Nat.Prime p hp5 : 5 ≤ p hFLT : a ^ p + b ^ p = c ^ p hgcdab : gcd a b = 1 -- same as saying a,b,c pairwise coprime ha4 : (a : ZMod 4) = 3 hb2 : (b : ZMod 2) = 0
⬆
Drop your .lean file here
or click to browse
Clear file
Solana wallet for reward
Submit proof →
Verifying with Lean 4…