The n-torsion of an elliptic curve has n² points #
Theorem statement: WeierstrassCurve.card_torsion_of_isAlgClosed
(11439a28-4f47-513e-b777-e6e7e1abad80), by Claude, 2026-09-05.
Proof: submission 0673979f-62c4-5f24-84e0-d46b480662a6, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ be a field, let $K$ be an algebraically closed field equipped with an $F$-algebra structure,
and let $W$ be a Weierstrass curve over $F$ which is elliptic (its discriminant is a unit). Let $n$
be a natural number whose image in $K$ is nonzero, i.e. the characteristic of $K$ does not divide
$n$; in particular $n \neq 0$. Write $W⁄K$ for the base change of $W$ along $F \to K$ and
$(W⁄K)$.Point for the group of $K$-points of the associated affine Weierstrass curve, consisting
of the point at infinity together with the nonsingular affine solutions, with its usual
chord-and-tangent group law, viewed as a $\mathbb{Z}$-module. The assertion is that the $n$-torsion
submodule $\{P : n \cdot P = 0\}$ of this group has exactly $n^2$ elements, in the sense that its
Nat.card equals $n^2$; since $n^2 \neq 0$, this includes the assertion that the $n$-torsion is
finite. This is the counting form of the statement $E[n] \cong (\mathbb{Z}/n\mathbb{Z})^2$: the
group structure of the $n$-torsion is not asserted here, only its cardinality.
This is the standard computation of the order of the $n$-torsion of an elliptic curve over an algebraically closed field of characteristic not dividing $n$, classically obtained from the division polynomials or from the degree of the multiplication-by-$n$ isogeny. It underlies the construction of the mod-$p$ and $p$-adic Galois representations attached to an elliptic curve, supplying the two-dimensionality of $E[p]$ over $\mathbb{F}_p$, and is used throughout the development downstream of the Galois-representation definitions.
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.lean
<!-- Generated by add_prove2me_provenance.py -->