The fixed field ℚ(a) of a canonical algebraic number: the presentation
ring on its minimal polynomial, with the embedding fixed by the root it
denotes. Reducible, so every PolyQuot operation, instance and theorem
applies unchanged.
29.5. A fixed field: ℚ(∛2)
If you are working in a fixed number field, use Hex.QAdjoin. Any
algebraic number converts into its own field with
Hex.AlgebraicNumber.toQAdjoin. Arithmetic and equality are efficient
there, since an element is just a rational polynomial in the generator
reduced modulo its minimal polynomial, and inverses are calculated with
extended gcds.
def cbrt2 : AlgebraicNumber :=
(ZPoly.algebraicRoots #p[-2, 0, 0, 1])[0]!
def c : QAdjoin cbrt2 := cbrt2.toQAdjoin
#guard c ^ 3 = 2
#guard c⁻¹ = c * c / 2
#guard c.toAlgebraicNumber = cbrt2
An element prints as the expression that rebuilds it: the generating number,
which prints round-trippably itself, and the coordinates, here c⁵ = 2c².
Pasting the output back reproduces the element:
#eval c ^ 5
-- the printed form, pasted back
#eval QAdjoin.ofCoeffs
(ZPoly.rootNear #p[-2, 0, 0, 1] 1.25992) #p[0, 0, 2]
#guard (c ^ 5).coeffs = #p[0, 0, 2]
The last check converts the coordinate form back to a canonical number and recovers the number it came from.
def