Mulders-Storjohann Correctness Reducer Minimality #
Least-row minimality and the certified reducer context.
theorem
CompPoly.PolynomialMatrix.muldersStorjohannReduce_least_row_minimal
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
(M : PolynomialMatrix F)
(shift : Array ℕ)
(row : PolynomialRow F)
(hM : M.WellFormed)
(hshift : shift.size = M.MatrixWidth)
(hrow : row ∈ M.RowSpan)
(hdeg : rowShiftedDegree? row shift ≠ none)
:
∃ (outRow : PolynomialRow F) (outDeg : ℕ) (rowDeg : ℕ),
outRow ∈ (M.muldersStorjohannReduce shift).MatrixRows ∧ rowShiftedDegree? outRow shift = some outDeg ∧ rowShiftedDegree? row shift = some rowDeg ∧ outDeg ≤ rowDeg
def
CompPoly.PolynomialMatrix.muldersStorjohannReducerContext
(F : Type u_2)
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
:
Certified direct Mulders-Storjohann shifted row-reducer context.