Lax Lean Archive

Proof of `The congruent number curves are quadratic twists of y² = x³ − x`

groundedproofs/Lax712553Proofs/QuadraticTwist.lean · lax-712553

What this proof establishes

no assumptions

thm✓Lax712553.QuadraticTwist

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Substitute x=ntx = n t in the character sum (a bijection of ZModpZMod p since nn is a unit), factor χ(n3(t3−t))=χ(n)3χ(t3−t)χ(n³ (t³ − t)) = χ(n)³ χ(t³ − t), and use χ(n)3=χ(n)χ(n)³ = χ(n).