n-torsion of an elliptic curve over an algebraically closed field #
Theorem statement: WeierstrassCurve.card_torsionBy_eq_sq_of_isAlgClosed
(f94c2d08-0249-52d5-8bc0-9de7ee84bbdd), by Claude, 2026-09-05.
Proof: submission 9b84a731-dcd8-5715-8d80-e882eb90298a, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ be an algebraically closed field with decidable equality, and let $W$ be a Weierstrass curve
over $F$ which is elliptic in the sense of Mathlib's IsElliptic, i.e. its discriminant is a unit.
Let $n$ be a natural number whose image in $F$ is nonzero, and assume also that $2 \ne 0$ in $F$.
Consider the group $W.toAffine.Point$ of points of the associated affine Weierstrass curve over $F$
— the points of the affine model together with the point at infinity, with its Mathlib group
structure — regarded as a $\mathbb{Z}$-module, and inside it the submodule
$\mathrm{torsionBy}\,\mathbb{Z}\,n$ of elements killed by $n$. The assertion is that this
$n$-torsion submodule is finite of cardinality exactly $n^2$, the equality being stated for
Nat.card. Note that the conclusion records only the order of $E[n]$, not the stronger isomorphism
$E[n] \cong (\mathbb{Z}/n)^2$.
This is the classical cardinality statement $\#E(F)[n] = n^2$ for an elliptic curve over an algebraically closed field of characteristic not dividing $n$ (Silverman, Corollary III.6.4(b)). It is the counting input behind the two-dimensionality of the mod-$n$ representations $\bar\rho_{E,n} \colon G_K \to \mathrm{GL}_2(\mathbb{Z}/n)$ attached to elliptic curves, and is invoked at several places in the Galois-representation part of the development.
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_torsionBy_eq_sq_of_isAlgClosed.lean
<!-- Generated by add_prove2me_provenance.py -->