Mulders-Storjohann Correctness Matrix Row Helpers

Replacement-row, matrix-shape, and row-span transport lemmas.

theorem CompPoly.PolynomialMatrix.replaceRow_size {F : Type u_1} [Field F] (M : PolynomialMatrix F) (idx : ℕ) (row : PolynomialRow F) : Array.size (M.replaceRow idx row) = Array.size M

theorem CompPoly.PolynomialMatrix.replaceRow_matrixWidth {F : Type u_1} [Field F] {M : PolynomialMatrix F} {idx : ℕ} {row : PolynomialRow F} (hrow : Array.size row = M.MatrixWidth) : (M.replaceRow idx row).MatrixWidth = M.MatrixWidth

theorem CompPoly.PolynomialMatrix.replaceRow_shape {F : Type u_1} [Field F] {M : PolynomialMatrix F} {idx : ℕ} {row : PolynomialRow F} (hrow : Array.size row = M.MatrixWidth) : (M.replaceRow idx row).MatrixShape = M.MatrixShape

theorem CompPoly.PolynomialMatrix.replaceRow_wellFormed {F : Type u_1} [Field F] {M : PolynomialMatrix F} {idx : ℕ} {row : PolynomialRow F} (hM : M.WellFormed) (hrow : Array.size row = M.MatrixWidth) : (M.replaceRow idx row).WellFormed

theorem CompPoly.PolynomialMatrix.replaceRow_rows_mem_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} (hM : M.WellFormed) {idx : ℕ} {newRow row : PolynomialRow F} (hnew : newRow ∈ M.RowSpan) (hrow : row ∈ (M.replaceRow idx newRow).MatrixRows) : row ∈ M.RowSpan

theorem CompPoly.PolynomialMatrix.replaceRow_newRow_mem {F : Type u_1} [Field F] {M : PolynomialMatrix F} {idx : ℕ} {newRow : PolynomialRow F} (hidx : idx < Array.size M) : newRow ∈ (M.replaceRow idx newRow).MatrixRows

theorem CompPoly.PolynomialMatrix.replaceRow_oldRow_mem {F : Type u_1} [Field F] {M : PolynomialMatrix F} {idx k : ℕ} {newRow : PolynomialRow F} (hk : k < Array.size M) (hne : idx ≠ k) : M[k] ∈ (M.replaceRow idx newRow).MatrixRows

theorem CompPoly.PolynomialMatrix.matrix_getD_size_of_wellFormed {F : Type u_1} [Field F] {M : PolynomialMatrix F} (hM : M.WellFormed) {i : ℕ} (hi : i < Array.size M) : Array.size (Array.getD M i #[]) = M.MatrixWidth

theorem CompPoly.PolynomialMatrix.matrix_getElem?_getD_size_of_wellFormed {F : Type u_1} [Field F] {M : PolynomialMatrix F} (hM : M.WellFormed) {i : ℕ} (hi : i < Array.size M) : Array.size (M[i]?.getD #[]) = M.MatrixWidth

theorem CompPoly.PolynomialMatrix.matrix_getD_mem_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} (hM : M.WellFormed) {i : ℕ} (hi : i < Array.size M) : Array.getD M i #[] ∈ M.RowSpan

theorem CompPoly.PolynomialMatrix.zeroRow_mem_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (hM : M.WellFormed) : zeroRow M.MatrixWidth ∈ M.RowSpan

theorem CompPoly.PolynomialMatrix.rowLinearCombination_mem_rowSpan_of_rows_mem {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {A B : PolynomialMatrix F} (hB : B.WellFormed) (hwidth : A.MatrixWidth = B.MatrixWidth) (hrows : ∀ row ∈ A.MatrixRows, row ∈ B.RowSpan) (coeffs : Array (CPolynomial F)) : rowLinearCombination coeffs A ∈ B.RowSpan

theorem CompPoly.PolynomialMatrix.rowSpan_subset_of_rows_mem {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {A B : PolynomialMatrix F} (hB : B.WellFormed) (hwidth : A.MatrixWidth = B.MatrixWidth) (hrows : ∀ row ∈ A.MatrixRows, row ∈ B.RowSpan) : A.RowSpan ⊆ B.RowSpan

theorem CompPoly.PolynomialMatrix.cancelShiftedLeadingTerm_size_of_wellFormed {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} (hM : M.WellFormed) {i j : ℕ} (hi : i < Array.size M) (hj : j < Array.size M) (shift : Array ℕ) : Array.size (cancelShiftedLeadingTerm (Array.getD M i #[]) (Array.getD M j #[]) shift) = M.MatrixWidth