Divisibility of E(K) for K algebraically closed #
Theorem statement: WeierstrassCurve.Affine.Point.exists_zsmul_eq_of_isAlgClosed
(1d8c7b68-f0ad-51eb-9206-a061eb7dd198), by Claude, 2026-09-05.
Proof: submission 7ca68070-cc9d-5e89-8eef-ee3e87bfa9b9, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be an algebraically closed field, $E$ a Weierstrass curve over $K$ which is elliptic (i.e.
carries the IsElliptic property: invertible discriminant), and let $n$ be a nonzero integer. Then
for every point $P$ of the group $E(K)$ of $K$-points of the associated affine Weierstrass curve —
that is, the affine points satisfying the Weierstrass equation together with the point at infinity,
with the usual chord-and-tangent group law — there exists a point $Q$ of $E(K)$ with $n \cdot Q = P$, the scalar action being the integer scalar multiplication of the additive group $E(K)$.
Equivalently, $E(K)$ is a divisible abelian group: multiplication by any nonzero integer is
surjective on the $K$-points of an elliptic curve over an algebraically closed field. No assumption
is made on the characteristic of $K$, and in particular $n$ is allowed to be divisible by it.
This is the classical statement that multiplication by $n \neq 0$ is surjective on the points of an elliptic curve over an algebraically closed field, the map $[n]$ being a non-constant, hence surjective, morphism of curves. It is used in the treatment of endomorphisms and isogenies of elliptic curves, for instance in the construction of dual isogeny data and in the analysis of the rank of endomorphism rings.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WeierstrassCurve_Affine_Point_exists_zsmul_eq_of_isAlgClosed.lean
<!-- Generated by add_prove2me_provenance.py -->