theorem Hex.AlgebraicPoly.roots?_isSome (f : AlgebraicPoly) : f.roots?.isSome = true

The algebraic-coefficient root driver always produces a checked root set.

theorem Hex.AlgebraicPoly.roots?_eq_roots (f : AlgebraicPoly) : f.roots? = some f.roots

The total algebraic-coefficient root API is exactly the output of its checked driver.

theorem Hex.AlgebraicPoly.roots_all_iff (f : AlgebraicPoly) : f.roots = RootSet.all ↔ f.toPolynomial = 0

The algebraic-coefficient driver returns .all exactly for the zero polynomial.

theorem Hex.AlgebraicPoly.contains_roots_iff (f : AlgebraicPoly) (z : ℂ) : f.roots.Contains z ↔ Polynomial.eval z f.toPolynomial = 0

Semantic membership in the algebraic-coefficient output is exactly polynomial vanishing.

theorem Hex.AlgebraicPoly.multiplicity_roots (f : AlgebraicPoly) (z : ℂ) : f.roots.multiplicityOf z = Polynomial.rootMultiplicity z f.toPolynomial

Algebraic-coefficient root multiplicities agree with Mathlib.

theorem Hex.AlgebraicPoly.roots_positive (f : AlgebraicPoly) : f.roots.Positive

The algebraic-coefficient driver produces positive multiplicities.

theorem Hex.AlgebraicPoly.roots_noDuplicates (f : AlgebraicPoly) : f.roots.NoDuplicates

The algebraic-coefficient driver merges all semantic duplicates.

theorem Hex.AlgebraicPoly.roots_ordered (f : AlgebraicPoly) : f.roots.Ordered

The algebraic-coefficient driver uses its deterministic canonical order.

theorem Hex.AlgebraicPoly.totalMultiplicity_roots (f : AlgebraicPoly) (hfPolynomial : f.toPolynomial ≠ 0) : f.roots.totalMultiplicity = f.toPolynomial.natDegree

For a nonzero algebraic-coefficient polynomial, output multiplicities sum to its degree.