theorem EllipticCurve.MordellWeil.canonical_height_exists (W : WeierstrassCurve ℚ) [W.IsElliptic] : ∃ (ĥ : W.toAffine.Point → ℝ), (∀ (P : W.toAffine.Point), 0 ≤ ĥ P) ∧ (∀ (P : W.toAffine.Point), ĥ (2 • P) = 4 * ĥ P) ∧ (∀ (P Q : W.toAffine.Point), ĥ (P + Q) + ĥ (P - Q) = 2 * ĥ P + 2 * ĥ Q) ∧ ∀ (B : ℝ), {P : W.toAffine.Point | ĥ P ≤ B}.Finite

Existence of the canonical (Néron-Tate) height on an elliptic curve over $\mathbb{Q}$: a function $\hat{h}$ that is nonnegative, satisfies $\hat{h}(2P) = 4\hat{h}(P)$, the parallelogram law $\hat{h}(P+Q) + \hat{h}(P-Q) = 2\hat{h}(P) + 2\hat{h}(Q)$, and the Northcott property (sublevel sets are finite).

theorem EllipticCurve.MordellWeil.mordell_weil_special (W : WeierstrassCurve ℚ) [W.IsElliptic] (data : WeakMordellWeil.TwoIsogenyData W) : AddGroup.FG W.toAffine.Point

Mordell-Weil theorem (special case): the group $E(\mathbb{Q})$ of an elliptic curve over $\mathbb{Q}$ admitting a 2-isogeny is finitely generated.

theorem EllipticCurve.MordellWeil.theorem_25_23 (W : WeierstrassCurve ℚ) [W.IsElliptic] (data : WeakMordellWeil.TwoIsogenyData W) : AddGroup.FG W.toAffine.Point

(Theorem 25.23, Mordell-Weil) Restatement: $E(\mathbb{Q})$ is finitely generated when there is a 2-isogeny.