29.7. The Mathlib correspondence🔗

The HexNumberFieldMathlib library interprets every representation in ℂ. Two canonical numbers with the same complex value are equal, and the computable operations on algebraic numbers match the operations in ℂ.

open Hex HexNumberFieldChapter

example (a b : AlgebraicNumber)
    (h : a.toComplex = b.toComplex) : a = b :=
  AlgebraicNumber.toComplex_injective h

example : (sqrt2 + sqrt3).toComplex =
    sqrt2.toComplex + sqrt3.toComplex :=
  AlgebraicNumber.add_toComplex sqrt2 sqrt3

-- The instance's operations are the executable ones.
example (a b : AlgebraicNumber) :
    a * b = AlgebraicNumber.mul a b := rfl
example (a : AlgebraicNumber) :
    a⁻¹ = AlgebraicNumber.inv a := rfl

The roots returned by Hex.ZPoly.algebraicRoots are exactly the complex roots of the polynomial, each once, and the reality test is exact:

theorem

Hex.ZPoly.mem_algebraicRoots_iff (p : Hex.ZPoly) (hp : p ≠ 0) (z : ℂ) :
  (∃ a ∈ p.algebraicRoots.toList, a.toComplex = z) ↔
    (HexRootsMathlib.toPolyℂ p).IsRoot z
Hex.ZPoly.mem_algebraicRoots_iff
  (p : Hex.ZPoly) (hp : p ≠ 0) (z : ℂ) :
  (∃ a ∈ p.algebraicRoots.toList,
      a.toComplex = z) ↔
    (HexRootsMathlib.toPolyℂ p).IsRoot z

The output lists exactly the roots of a nonzero polynomial.

theorem

Hex.AlgebraicNumber.isReal_iff (a : Hex.AlgebraicNumber) :
  a.isReal = true ↔ a.toComplex.im = 0
Hex.AlgebraicNumber.isReal_iff
  (a : Hex.AlgebraicNumber) :
  a.isReal = true ↔ a.toComplex.im = 0

The reality test is exact at the stored separation precision.

theorem

Hex.AlgebraicPoly.contains_roots_iff (f : Hex.AlgebraicPoly) (z : ℂ) :
  f.roots.Contains z ↔ Polynomial.eval z f.toPolynomial = 0
Hex.AlgebraicPoly.contains_roots_iff
  (f : Hex.AlgebraicPoly) (z : ℂ) :
  f.roots.Contains z ↔
    Polynomial.eval z f.toPolynomial = 0

Semantic membership in the algebraic-coefficient output is exactly polynomial vanishing.

For a checked fixed presentation, the coordinates of Hex.QAdjoin are ring-equivalent to Mathlib's AdjoinRoot of the defining polynomial, and opening the scope Hex.PolyQuot.QAdjoinField gives them Mathlib's field notation and laws, noncomputably; executable code keeps the unscoped operations.