def Hex.FpPoly.squareFreeAuxRev {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (multiplicity : Nat) : Nat → List (SquareFreeFactor p) → List (SquareFreeFactor p)

Tail-recursive square-free decomposition over F_p[x], accumulating factors in reverse output order. A derivative-zero branch descends through the formal p-th root and scales multiplicities by p.

Equations

• One or more equations did not get rendered due to their size.
• f.squareFreeAuxRev multiplicity 0 x✝ = x✝

def Hex.FpPoly.squareFreeAux {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (multiplicity fuel : Nat) : List (SquareFreeFactor p)

Recursive square-free decomposition over F_p[x]. A derivative-zero branch descends through the formal p-th root and scales multiplicities by p.

Equations

• f.squareFreeAux multiplicity fuel = (f.squareFreeAuxRev multiplicity fuel []).reverse