theorem Hex.AlgebraicPoly.Common.extend?_degree (theta alpha gamma : AlgebraicNumber) (hgamma : extend? theta alpha = some gamma) : degree gamma = Module.finrank ℚ ↥ℚ⟮theta.toComplex, alpha.toComplex⟯

A successful maximum-degree shift search reaches the full compositum degree.

theorem Hex.AlgebraicPoly.Common.extend?_field (theta alpha gamma : AlgebraicNumber) (hgamma : extend? theta alpha = some gamma) : ℚ⟮gamma.toComplex⟯ = ℚ⟮theta.toComplex, alpha.toComplex⟯

The maximum-degree shift returned by extend? generates exactly the compositum of its two inputs.

theorem Hex.AlgebraicPoly.Common.extendShift?_field (theta alpha : AlgebraicNumber) (shifted : ShiftCandidate) (hshifted : extendShift? theta alpha = some shifted) : ℚ⟮shifted.value.toComplex⟯ = ℚ⟮theta.toComplex, alpha.toComplex⟯

The shift-retaining maximum-degree candidate generates the same compositum as the two inputs.

theorem Hex.AlgebraicPoly.Common.primitive?_contains (coefficients : Array AlgebraicNumber) (gamma a : AlgebraicNumber) (hgamma : primitive? coefficients = some gamma) (ha : a ∈ coefficients) : a.toComplex ∈ ℚ⟮gamma.toComplex⟯

Every input coefficient belongs to the simple field selected by a successful primitive-element fold.