noncomputable def Hex.AlgebraicNumber.rootKey (a : AlgebraicNumber) : Lex (ℕ × Lex (ℚ × Lex (ℚ × Lex (ℤ × Lex (List ℤ × ℕ)))))

The deterministic enumeration key, distinct from the complex partial order.

Equations

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

theorem Hex.AlgebraicNumber.rootLe_iff (a b : AlgebraicNumber) : a.rootLe b = true ↔ a.rootKey ≤ b.rootKey

The executable enumeration comparator is lexicographic comparison of its key.

theorem Hex.AlgebraicNumber.rootLe_trans (a b c : AlgebraicNumber) (hab : a.rootLe b = true) (hbc : b.rootLe c = true) : a.rootLe c = true

Enumeration comparison is transitive.

theorem Hex.AlgebraicNumber.rootLe_total (a b : AlgebraicNumber) : (a.rootLe b || b.rootLe a) = true

Any two canonical numbers are comparable for enumeration.

theorem Hex.AlgebraicNumber.eq_of_rootKey {a b : AlgebraicNumber} (ha : a.isReal = false) (hb : b.isReal = false) (h : a.rootKey = b.rootKey) : a = b

Nonreal enumeration keys determine the canonical value.

theorem Hex.AlgebraicNumber.rootLe_conj (a : AlgebraicNumber) (ha : a.side = RootSide.lower) : a.rootLe a.conj = true

The lower member precedes its upper conjugate.

theorem Hex.AlgebraicNumber.between_conjugates (a b : AlgebraicNumber) (ha : a.side = RootSide.lower) (hab : a.rootLe b = true) (hba : b.rootLe a.conj = true) : b = a ∨ b = a.conj

A nonreal lower root and its conjugate have no other canonical value between them.

theorem Hex.ZPoly.algebraicRoots_sorted (p : ZPoly) : List.Pairwise (fun (a b : AlgebraicNumber) => a.rootLe b = true) p.algebraicRoots.toList

Integer root enumeration is sorted by its canonical centre key.

theorem Hex.ZPoly.conj_mem_algebraicRoots {p : ZPoly} (hp : p ≠ 0) {a : AlgebraicNumber} (ha : a ∈ p.algebraicRoots) : a.conj ∈ p.algebraicRoots

The conjugate of every listed root is listed too.