The minimal polynomial of over is the depressed cubic
ProvedCollapsibleCubics.minpoly_int_thetaOalgebraic-number-theorynumber-theory
Let with irreducible over , and let be the root of that cubic in . Then the minimal polynomial of over is exactly in .
This identifies the integral model, which is what lets Kummer-Dedekind's factorisation of be read off from the factorisation of modulo .
Preamble
import Mathlib import Definitions.Def_CollapsibleCubics_q7
Formal statement
namespace CollapsibleCubics
open NumberField
theorem minpoly_int_thetaO (D E : ℤ) [Fact (Irreducible (cubicPoly (D : ℚ) (E : ℚ)))] :
minpoly ℤ (thetaO D E) = cubicPolyInt D E := by sorry
end CollapsibleCubicsSource
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/