theorem Hex.AlgebraicPoly.Common.degree_dvd_of_mem (gamma a : AlgebraicNumber) (ha : a.toComplex ∈ ℚ⟮gamma.toComplex⟯) : degree a ∣ degree gamma

The degree of an algebraic number lying in a primitive field divides the degree of that field.

theorem Hex.AlgebraicPoly.Common.trace?_isSome (gamma a : AlgebraicNumber) (ha : a.toComplex ∈ ℚ⟮gamma.toComplex⟯) : (trace? (degree gamma) a).isSome = true

Trace succeeds whenever the input belongs to the stated primitive field.

theorem Hex.AlgebraicPoly.Common.trace?_sound (gamma a : AlgebraicNumber) (ha : a.toComplex ∈ ℚ⟮gamma.toComplex⟯) {t : ℚ} (h : trace? (degree gamma) a = some t) : t = (Algebra.trace ℚ ↥ℚ⟮gamma.toComplex⟯) ⟨a.toComplex, ha⟩

A successful executable trace is the field trace from the primitive ambient field.

theorem Hex.AlgebraicPoly.Common.coordinates?_isSome (gamma a : AlgebraicNumber) (powers : Array AlgebraicNumber) (hsize : powers.size = 2 * degree gamma - 1) (hvalues : ∀ (i : ℕ) (hi : i < powers.size), powers[i].toComplex = gamma.toComplex ^ i) (ha : a.toComplex ∈ ℚ⟮gamma.toComplex⟯) : (coordinates? gamma a powers).isSome = true

Coordinate recovery succeeds for an element of the primitive field when the supplied table contains the required consecutive powers.

theorem Hex.AlgebraicPoly.Common.coordinates?_sound (gamma a : AlgebraicNumber) (powers : Array AlgebraicNumber) {coordinate : PolyQuot gamma.p gamma.x} (h : coordinates? gamma a powers = some coordinate) : coordinate.toComplex gamma.rep ⋯ = a.toComplex

Successful coordinate recovery represents the original algebraic value at the selected primitive embedding.