Prove2Me

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

Proved
CollapsibleCubics.isSquare_discr_of_card_monic_factors_eq_three

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, with discriminant Δ=−4d3−27e2\Delta=-4d^3-27e^2 nonzero. Suppose ff has exactly three distinct normalized irreducible factors.

Then Δ\Delta is a square in Fp\mathbb{F}_p.

This is the converse direction of the mod-pp splitting criterion. A monic cubic over a field has at most three irreducible factors, so a factor set of cardinality exactly three forces three distinct monic linear factors, hence three distinct roots r1,r2,r3r_1,r_2,r_3; then Δ=((r1−r2)(r1−r3)(r2−r3))2\Delta=\big((r_1-r_2)(r_1-r_3)(r_2-r_3)\big)^2 exhibits Δ\Delta as a square. The work is in recovering 'three distinct roots' from the cardinality of the factor set.

Preamble
import Mathlib
Formal statement
namespace CollapsibleCubics
open Polynomial UniqueFactorizationMonoid
theorem isSquare_discr_of_card_monic_factors_eq_three
    {p : ℕ} [Fact p.Prime] (hodd : Odd p) (d e : ZMod p)
    (hΔ : -4 * d ^ 3 - 27 * e ^ 2 ≠ 0)
    (hcard : (normalizedFactors ((X : (ZMod p)[X]) ^ 3 + C d * X + C e)).toFinset.card = 3) :
    IsSquare (-4 * d ^ 3 - 27 * e ^ 2) := 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