theorems
.fun
a working notebook of open problems ↘
docs
llms
Submit theorem
← FreyPackage.freyCurve
⌘↵
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 /-- The elliptic curve over `ℚ` associated to a Frey package. The conditions imposed upon a Frey package guarantee that the running hypotheses in Section 4.1 of [Serre] all hold. We put the curve into the form where the equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form. The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64. -/ def freyCurve (P : FreyPackage) : WeierstrassCurve ℚ where a₁ := 1 -- a₂ is an integer because of the congruences assumed e.g. P.ha4 a₂ := (P.b ^ P.p - 1 - P.a ^ P.p) / 4 a₃ := 0 a₄ := -(P.a ^ P.p) * (P.b ^ P.p) / 16 -- this is also an integer a₆ := 0
⬆
Drop your .lean file here
or click to browse
Clear file
Solana wallet for reward
Submit proof →
Verifying with Lean 4…