theorem Hex.ZPoly.algebraicRoots?_isSome (p : ZPoly) : p.algebraicRoots?.isSome = true

The root-set computation always produces a certificate.

theorem Hex.ZPoly.algebraicRoots?_eq (p : ZPoly) : p.algebraicRoots? = some p.algebraicRoots

The total wrapper is the checked computation.

theorem Hex.ZPoly.mem_algebraicRoots_iff (p : ZPoly) (hp : p ≠ 0) (z : ℂ) : (∃ a ∈ p.algebraicRoots.toList, a.toComplex = z) ↔ (HexRootsMathlib.toPolyℂ p).IsRoot z

The output lists exactly the roots of a nonzero polynomial.

theorem Hex.ZPoly.algebraicRoots_nodup (p : ZPoly) : p.algebraicRoots.toList.Nodup

The output has no repeated value.

theorem Hex.AlgebraicNumber.toQAdjoin_toComplex (a : AlgebraicNumber) : PolyQuot.toComplex a.toQAdjoin a.rep ⋯ = a.toComplex

The fixed-field coordinates of a canonical number evaluate to its value.

theorem Hex.AlgebraicNumber.approx_mem (a : AlgebraicNumber) (prec : ℤ) : a.toComplex ∈ (a.approx prec).set

The approximation ball contains the represented value.

theorem Hex.AlgebraicNumber.approx_radius (a : AlgebraicNumber) (prec : ℤ) : (a.approx prec).realRadius ≤ 2 ^ (-prec)

The approximation ball has the requested radius.

theorem Hex.AlgebraicNumber.isRoot_conj {p : ZPoly} {z : ℂ} (hz : (HexRootsMathlib.toPolyℂ p).IsRoot z) : (HexRootsMathlib.toPolyℂ p).IsRoot ((starRingEnd ℂ) z)

Compatibility name for conjugate closure, now proved in HexRootsMathlib.

theorem Hex.AlgebraicNumber.isReal_iff (a : AlgebraicNumber) : a.isReal = true ↔ a.toComplex.im = 0

The reality test is exact at the stored separation precision.

theorem Hex.AlgebraicNumber.side_upper_iff (a : AlgebraicNumber) : a.side = RootSide.upper ↔ 0 < a.toComplex.im

The upper tag is exactly positivity of the imaginary coordinate.