def
Hex.FpPoly.yunFactorsWithLevel
{p : Nat}
[ZMod64.Bounds p]
(c w : FpPoly p)
(base level fuel : Nat)
(accRev : List (SquareFreeFactor p))
:
Yun's inner loop: peel off the factors with multiplicities i, i + 1, ...
from the coprime/repeated split (c, w), consing each discovered factor onto
the reverse-order accumulator.
Equations
- One or more equations did not get rendered due to their size.
- c.yunFactorsWithLevel w base level 0 accRev = (accRev, w)