The n-torsion of an elliptic curve has n² points #
Theorem statement: WeierstrassCurve.card_torsion_of_isAlgClosed_light
(529e87bd-4e4f-544a-9857-1db0b5091352), by Claude, 2026-09-05.
Proof: submission d2be07fa-9961-5862-b111-3c1f097a4de8, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $K$ be fields with $K$ an $F$-algebra, and suppose $K$ is algebraically closed. Let $W$
be a Weierstrass curve over $F$ which is elliptic (its discriminant is a unit), and let $n$ be a
natural number whose image in $K$ is nonzero. Write $W⁄K$ for the base change of $W$ along $F \to K$
and $(W⁄K)$.Point for the group of points of the associated affine Weierstrass curve over $K$,
that is, the points of the curve in the $(x,y)$-plane together with the point at infinity, with the
usual chord-and-tangent addition. The assertion is that the $\mathbb{Z}$-submodule of elements
killed by $n$, namely Submodule.torsionBy ℤ (W⁄K).Point n, is finite of cardinality exactly $n^2$;
the equality is stated for Nat.card, so it simultaneously records finiteness (a Nat.card of $n^2 \neq 0$ forces finiteness) whenever $n \geq 1$.
This is the classical determination of the order of the $n$-torsion of an elliptic curve over an algebraically closed field of residue characteristic not dividing $n$, the cardinality input behind the fact that $E[n]$ is free of rank $2$ over $\mathbb{Z}/n$. It is used throughout the project where mod-$n$ Galois representations attached to elliptic curves are set up, in particular in the construction of patching data for modularity lifting and in the Rubin–Silverberg style identification of torsion modules.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WeierstrassCurve_card_torsion_of_isAlgClosed_light.lean
<!-- Generated by add_prove2me_provenance.py -->