def Hex.NumberTower.checkFactorization {T : NumberTower} (f : T.Poly) (scalar : T.Elem) (factors : Array (T.Poly × Nat)) : Bool

Reconstruct and recursively certify a proposed public factorization.

Equations

• One or more equations did not get rendered due to their size.

structure Hex.NumberTower.Factorization (T : NumberTower) (f : T.Poly) : Type

A checked complete factorization in a fixed tower.

• scalar : T.Elem

  The leading scalar; the listed factors are monic.

• factors : Array (T.Poly × Nat)

  Monic irreducible factors, canonically sorted, each with its positive multiplicity.

• checked : checkFactorization f self.scalar self.factors = true

  The reconstruction and recursive irreducibility replay succeeded.

def Hex.NumberTower.factor? {T : NumberTower} (f : T.Poly) : Option (T.Factorization f)

Complete irreducible factorization with multiplicity.

Equations

• One or more equations did not get rendered due to their size.