A prime dividing the binary cubic form gives a root mod $p$

Proved

CollapsibleCubics.exists_root_of_prime_dvd_form

by quesswho · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-number-theorynumber-theory

Let $d,e,a,b\in\mathbb{Z}$ with $\gcd(a,b)=1$ , and let $p$ be a prime dividing the binary form $F(a,b)=a^3+dab^2+eb^3$ . Then the depressed cubic $x^3+dx+e$ has a root in $\mathbb{Z}/p$ .

The argument: coprimality forces $p\nmid b$ , so $b$ is invertible mod $p$ and $r=a b^{-1}$ is a root of $x^3+dx+e$ over $\mathbb{Z}/p$ , since $F(a,b)\equiv b^3\,(r^3+dr+e)$ .

Preamble

import Mathlib

Formal statement

namespace CollapsibleCubics
theorem exists_root_of_prime_dvd_form {p : ℕ} (hp : p.Prime) (d e a b : ℤ)
    (hab : IsCoprime a b) (h : (p : ℤ) ∣ a ^ 3 + d * a * b ^ 2 + e * b ^ 3) :
    ∃ r : ZMod p, r ^ 3 + (d : ZMod p) * r + (e : ZMod p) = 0 := by sorry
end CollapsibleCubics

Source

Collapsible Cubics mission (Q7 support chain); proved in the project repo, restated here for the platform. Background: https://quesswho.github.io/miles-blog/2026/08/20/collapsible/

View graph

A prime dividing the binary cubic form gives a root mod ppp

A prime dividing the binary cubic form gives a root mod $p$