def WeakMordellWeil.onCurveE (a b x y : ℚ) : Prop

Affine equation of the elliptic curve $E : y^2 = x(x^2 + ax + b)$, used in the descent step of the Mordell-Weil theorem (Chapter 25).

def WeakMordellWeil.onCurveE' (a b X Y : ℚ) : Prop

Affine equation of the 2-isogenous curve $E' : Y^2 = X(X^2 - 2aX + (a^2 - 4b))$ used as the target of the 2-isogeny $\varphi : E \to E'$.

def WeakMordellWeil.inImageOfPhi (a b X Y : ℚ) : Prop

A point $(X, Y) \in E'(\mathbb{Q})$ lies in the image of the 2-isogeny $\varphi : E \to E'$ if there exists $(x, y) \in E(\mathbb{Q})$ with $x \neq 0$, $X = x + a + b/x$ and $Y = y(1 - b/x^2)$.

def WeakMordellWeil.mem_QxSq (X : ℚ) : Prop

Membership predicate $X \in \mathbb{Q}^{\times 2}$: the rational $X$ is nonzero and a square.

theorem WeakMordellWeil.lemma_25_3 (a b X Y : ℚ) (hb : b ≠ 0) (hdisc : a ^ 2 - 4 * b ≠ 0) (hE' : onCurveE' a b X Y) : inImageOfPhi a b X Y ↔ mem_QxSq X ∨ X = 0 ∧ mem_QxSq (a ^ 2 - 4 * b)

Lemma 25.3 (image of the 2-isogeny). Assuming $b \neq 0$ and $a^2 - 4b \neq 0$, a point $(X, Y) \in E'(\mathbb{Q})$ lies in $\varphi(E(\mathbb{Q}))$ if and only if either $X$ is a nonzero square in $\mathbb{Q}$, or $X = 0$ and $a^2 - 4b$ is a nonzero square.

theorem WeakMordellWeil.sqfree_divisors_finite (B : ℤ) (hB : B ≠ 0) : {r : ℤ | Squarefree r ∧ r ∣ B}.Finite

Finiteness ingredient for the descent: the set of squarefree integer divisors of any nonzero $B \in \mathbb{Z}$ is finite.

theorem WeakMordellWeil.corollary_25_6 (a b : ℤ) (hb : b ≠ 0) (hdisc : a ^ 2 - 4 * b ≠ 0) : {r : ℤ | Squarefree r ∧ r ∣ a ^ 2 - 4 * b}.Finite ∧ {r : ℤ | Squarefree r ∧ r ∣ 16 * b}.Finite

Corollary 25.6 (finiteness for descent). The sets of squarefree divisors of $a^2 - 4b$ and of $16 b$ are both finite, providing the finite quotient $E(\mathbb{Q}) / 2 E(\mathbb{Q})$ needed in the Mordell-Weil theorem.