theorem Hex.AlgebraicPoly.Common.presentation?_isSome (coefficients : Array AlgebraicNumber) (hnonzero : ∃ a ∈ coefficients.toList, a.isZero = false) : (presentation? coefficients).isSome = true

A nonzero algebraic coefficient array always admits a checked primitive fixed-field presentation.

theorem Hex.AlgebraicPoly.Common.presentation?_sound (coefficients : Array AlgebraicNumber) {presentation : Presentation} (h : presentation? coefficients = some presentation) : presentation.coefficients.size = coefficients.size ∧ ∀ (i : ℕ) (hi : i < coefficients.size) (hiPresentation : i < presentation.coefficients.size), presentation.coefficients[i].toComplex presentation.generator.rep ⋯ = coefficients[i].toComplex

A successful presentation preserves the coefficient array length and the selected complex value of every coefficient.