theorem HexRootsMathlib.RefinedIsolation.root_heq {p q : Hex.ZPoly} (hp : p = q) {r : Hex.RefinedIsolation p} {s : Hex.RefinedIsolation q} (h : r ≍ s) : r.root = s.root

Equal dependent isolation data select equal roots.

@[simp]

theorem HexRootsMathlib.RefinedIsolation.root_conj {p : Hex.ZPoly} (a : Hex.RefinedIsolation p) : a.conj.root = (starRingEnd ℂ) a.root

Reflecting the isolation conjugates its unique root.

theorem HexRootsMathlib.RefinedIsolation.meetsRealAxis_iff {p : Hex.ZPoly} (a : Hex.RefinedIsolation p) : (↑a).square.meetsRealAxis = true ↔ a.root.im = 0

The reality test is exact at the stored separation precision.

theorem HexRootsMathlib.RefinedIsolation.upper_iff {p : Hex.ZPoly} (a : Hex.RefinedIsolation p) : (↑a).square.radiusHi < (↑a).square.im ↔ 0 < a.root.im

The stored upper-half-plane test is exact.