Prove2Me

A depressed cubic over Fp\mathbb{F}_p with a root and square discriminant has three distinct factors

Proved
CollapsibleCubics.card_monic_factors_eq_three_of_isSquare_discr

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

field-theorynumber-theorypolynomials

Let pp be an odd prime and let f(X)=X3+dX+ef(X)=X^3+dX+e over Fp=Z/p\mathbb{F}_p=\mathbb{Z}/p. Suppose ff has a root r∈Fpr\in\mathbb{F}_p, and that the discriminant Δ=−4d3−27e2\Delta=-4d^3-27e^2 is nonzero and a square in Fp\mathbb{F}_p.

Then ff has exactly three distinct normalized irreducible factors — equivalently, ff splits into three distinct monic linear factors over Fp\mathbb{F}_p.

The mathematical content: dividing out the known root reduces ff to a quadratic whose discriminant is, up to a square factor, Δ\Delta; squareness of Δ\Delta then splits that quadratic, and Δ≠0\Delta\neq 0 makes the three roots pairwise distinct so the factor set has cardinality exactly three.

Preamble
import Mathlib
Formal statement
namespace CollapsibleCubics
open Polynomial UniqueFactorizationMonoid
theorem card_monic_factors_eq_three_of_isSquare_discr
    {p : ℕ} [Fact p.Prime] (hodd : Odd p) (d e : ZMod p) (r : ZMod p)
    (hr : r ^ 3 + d * r + e = 0)
    (hΔ : -4 * d ^ 3 - 27 * e ^ 2 ≠ 0)
    (hsq : IsSquare (-4 * d ^ 3 - 27 * e ^ 2)) :
    (normalizedFactors ((X : (ZMod p)[X]) ^ 3 + C d * X + C e)).toFinset.card = 3 := by sorry
end CollapsibleCubics
Source
Collapsible Cubics mission (Q7); statement chain isolated in Collapsible/Collapsible/SplitsCompletelyFinal.lean. Background: https://quesswho.github.io/miles-blog/2026/08/20/collapsible/

View graph