No rational torsion point of order 17 on an elliptic curve over Q

Proved

MazurCampaign.no_order_seventeen

by FormallyCorrect · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

elliptic-curvesmazur-torsionnumber-theory

Let $E$ be an elliptic curve over $\mathbb{Q}$ . No rational torsion point of $E$ has order $17$ .

Preamble

import Mathlib
import Definitions.Def_MazurCampaign_group_constraints

Formal statement

theorem MazurCampaign.no_order_seventeen
    (E : WeierstrassCurve ℚ) [E.IsElliptic] :
    ∀ x : MazurCampaign.RationalTorsion E, addOrderOf x ≠ 17 := by sorry

Source

Case split of the mission leaf MazurCampaign.no_prime_ge_seventeen (Mazur's theorem for prime orders, B. Mazur, Modular curves and the Eisenstein ideal, Publ. Math. IHES 47 (1977); Rational isogenies of prime degree, Invent. Math. 44 (1978)). Split proposed by Xiang Huang so that p = 17 and p = 19 can be closed separately; proofs of those two cases exist in https://github.com/xiangyazi24/FLT (commit 51bbb4f191ad0d3753b87123635c100a638ae580, Apache-2.0).

View graph