Diagonal Modular Equation Solver Context #
Umbrella module for the diagonal modular-equation solver: definitions,
soundness, the completeness development, and the production
ModularSolutionBasisContext instance backed by the X-adic PM-basis.
def
CompPoly.PolynomialMatrix.Approximant.modularSolutionBasisContextViaPMBasis
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
(mulCtx : CPolynomial.MulContext F)
(modCtx : CPolynomial.ModContext F)
(pmCtx : PMBasisContext F)
:
Diagonal modular-equation solution-basis context obtained from the exact-nullspace lift and an X-adic PM-basis context.