def HexRealRootsMathlib.RealRootCount.termReal_root_count_ : Lean.ParserDescr

Compute and certify the number of distinct real roots of a closed squarefree integer-coefficient polynomial over ℚ of positive degree.

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.RealRootCount.tacticReal_root_count : Lean.ParserDescr

Prove a goal Fintype.card (p.rootSet ℝ) = n by a checked Sturm chain. The polynomial must be closed, squarefree, of positive degree, and have integer coefficients.

Equations

• One or more equations did not get rendered due to their size.