Canonicalize a lazy root: the total form of exact?, whose none branch
the Mathlib companion proves unreachable.
29.3. Lazy roots and exactification
Canonical arithmetic is built on a cheaper intermediate form. Adding two lazy
roots builds the resultant whose roots are all sums of a root of the first
polynomial with a root of the second, and isolates the one that is the actual
sum; nothing is factored. The sum of √2 with itself is a root of
X³ − 8X, whose three roots 0, ±2√2 are the sums of pairs of conjugates.
Requesting the canonical form factors that polynomial and keeps X² − 8:
def lazySum : AlgebraicRoot :=
sqrt2.toRoot.add sqrt2.toRoot
#guard lazySum.p = #p[0, -8, 0, 1]
#guard lazySum.exact.p = #p[-8, 0, 1]
def lazyProduct : AlgebraicRoot :=
sqrt2.toRoot.mul sqrt2.toRoot
#guard lazyProduct.p = #p[-4, 0, 1]
#guard lazyProduct.exact.p = #p[-2, 1]
#guard lazyProduct.exact = 2
A chain of lazy operations therefore costs a chain of resultants and one factorization at the end, instead of a factorization at every step. Canonical numbers use the same route and exactify each result, which is what makes their equality decidable.
def