Goal
Define the Frey curve E_{a,b} : y² = x(x − a)(x + b) of a coprime triple a + b = c as a WeierstrassCurve ℚ (or EllipticCurve ℚ), and compute its discriminant Δ = 16 (abc)².
What already exists
- mathlib:
WeierstrassCurve, EllipticCurve, WeierstrassCurve.Δ, j. Blueprint: ec.q.frey.
What's missing
- The named Frey curve as a Weierstrass model from
(a,b); its discriminant and j-invariant in terms of a,b,c. (Its conductor = rad(abc)-type statement depends on the conductor issue.)
Test cases
Δ(E_{a,b}) = 16 (a·b·(a+b))²; minimal model for a concrete coprime (a,b).
References
Blueprint & LMFDB targets
Rendered blueprint: https://cbirkbeck.github.io/LeanBridge/ — the definitions / LMFDB knowls this issue feeds.
Goal
Define the Frey curve
E_{a,b} : y² = x(x − a)(x + b)of a coprime triplea + b = cas aWeierstrassCurve ℚ(orEllipticCurve ℚ), and compute its discriminantΔ = 16 (abc)².What already exists
WeierstrassCurve,EllipticCurve,WeierstrassCurve.Δ,j. Blueprint:ec.q.frey.What's missing
(a,b); its discriminant andj-invariant in terms ofa,b,c. (Its conductor =rad(abc)-type statement depends on the conductor issue.)Test cases
Δ(E_{a,b}) = 16 (a·b·(a+b))²; minimal model for a concrete coprime(a,b).References
Blueprint & LMFDB targets
ec.q.frey— blueprint · LMFDBRendered blueprint: https://cbirkbeck.github.io/LeanBridge/ — the definitions / LMFDB knowls this issue feeds.