Coprimality of the division polynomials Φₙ and Ψₙ² #
Theorem statement: WeierstrassCurve.isCoprime_Phi_PsiSq (0f9a1d23-7366-54ec-bbbd-9af4a5dd2cbd),
by Claude, 2026-09-05.
Proof: submission 9d37f4a8-1614-59d3-9a16-51a875770dce, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ be a field and let $W$ be a Weierstrass curve over $F$ which is elliptic, i.e. whose
discriminant is a unit, and let $n$ be an arbitrary integer (no sign condition, and no condition on
$n$ modulo the characteristic of $F$). The assertion is that the two univariate division polynomials
attached to $W$ and $n$ in Mathlib's notation, namely W.Φ n and W.ΨSq n — the numerator and the
denominator of the $x$-coordinate of multiplication by $n$, so that $x \circ [n] = \Phi_n/\Psi_n^2$
as a rational function — are coprime as elements of the polynomial ring $F[X]$, in the sense of
IsCoprime: there exist polynomials $a, b \in F[X]$ with $a\,\Phi_n + b\,\Psi_n^2 = 1$. Over a
field this is equivalent to the vanishing of the greatest common divisor condition $\gcd(\Phi_n, \Psi_n^2) = 1$, and it includes the degenerate cases $n = 0, \pm 1$, where one of the two
polynomials is a unit.
This is the classical statement that the representation $x \circ [n] = \Phi_n/\Psi_n^2$ of the multiplication-by-$n$ map is in lowest terms, which is what makes the degree of $[n]$ readable off the degrees of $\Phi_n$ and $\Psi_n^2$. It is used throughout the treatment of isogeny degrees and kernels, for instance in the computation of degrees of Frobenius endomorphisms and in the description of kernel ideals of quaternionic 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_isCoprime_Phi_PsiSq.lean
<!-- Generated by add_prove2me_provenance.py -->