Shifted Row Reduction Contexts

structure CompPoly.PolynomialMatrix.ShiftedRowReducerContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] : Type u_1

Executable shifted row-reduction backend over F[X].

• reduce : PolynomialMatrix F → Array ℕ → PolynomialMatrix F
• shape_preserved (M : PolynomialMatrix F) (shift : Array ℕ) : M.WellFormed → (self.reduce M shift).MatrixShape = M.MatrixShape
• rowSpan_eq (M : PolynomialMatrix F) (shift : Array ℕ) : M.WellFormed → (self.reduce M shift).RowSpan = M.RowSpan
• weakPopov (M : PolynomialMatrix F) (shift : Array ℕ) : M.WellFormed → shift.size = M.MatrixWidth → (self.reduce M shift).ShiftedWeakPopov shift
• least_row_minimal (M : PolynomialMatrix F) (shift : Array ℕ) (row : PolynomialRow F) : M.WellFormed → shift.size = M.MatrixWidth → row ∈ M.RowSpan → rowShiftedDegree? row shift ≠ none → ∃ (outRow : PolynomialRow F) (outDeg : ℕ) (rowDeg : ℕ), outRow ∈ (self.reduce M shift).MatrixRows ∧ rowShiftedDegree? outRow shift = some outDeg ∧ rowShiftedDegree? row shift = some rowDeg ∧ outDeg ≤ rowDeg