Mulders-Storjohann Correctness Row and Row-Span Helpers

Row operation and row-span lemmas used by the Mulders-Storjohann correctness proof.

theorem CompPoly.PolynomialMatrix.rowScalePolynomial_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : CPolynomial F) (row : PolynomialRow F) : Array.size (rowScalePolynomial c row) = Array.size row

theorem CompPoly.PolynomialMatrix.rowScaleMonomial_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (c : F) (d : ℕ) (row : PolynomialRow F) : Array.size (rowScaleMonomial c d row) = Array.size row

theorem CompPoly.PolynomialMatrix.rowNeg_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) : Array.size (rowNeg row) = Array.size row

theorem CompPoly.PolynomialMatrix.rowAdd_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (a b : PolynomialRow F) : Array.size (rowAdd a b) = max (Array.size a) (Array.size b)

theorem CompPoly.PolynomialMatrix.rowSub_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (a b : PolynomialRow F) : Array.size (rowSub a b) = max (Array.size a) (Array.size b)

theorem CompPoly.PolynomialMatrix.rowGet_rowAdd {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (a b : PolynomialRow F) (j : ℕ) : rowGet (rowAdd a b) j = rowGet a j + rowGet b j

theorem CompPoly.PolynomialMatrix.rowGet_rowScalePolynomial {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : CPolynomial F) (row : PolynomialRow F) (j : ℕ) : rowGet (rowScalePolynomial c row) j = c * rowGet row j

theorem CompPoly.PolynomialMatrix.rowGet_rowNeg {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) (j : ℕ) : rowGet (rowNeg row) j = -rowGet row j

theorem CompPoly.PolynomialMatrix.rowGet_rowSub {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (a b : PolynomialRow F) (j : ℕ) : rowGet (rowSub a b) j = rowGet a j - rowGet b j

theorem CompPoly.PolynomialMatrix.rowGet_rowScaleMonomial {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (c : F) (d : ℕ) (row : PolynomialRow F) (j : ℕ) : rowGet (rowScaleMonomial c d row) j = CPolynomial.monomial d c * rowGet row j

theorem CompPoly.PolynomialMatrix.rowGet_zeroRow {F : Type u_1} [Field F] (width j : ℕ) : rowGet (zeroRow width) j = 0

theorem CompPoly.PolynomialMatrix.rowScalePolynomial_zeroRow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : CPolynomial F) (width : ℕ) : rowScalePolynomial c (zeroRow width) = zeroRow width

theorem CompPoly.PolynomialMatrix.rowScalePolynomial_eq_zeroRow_of_rowIsZero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : CPolynomial F) {row : PolynomialRow F} (hrow : RowIsZero row) : rowScalePolynomial c row = zeroRow (Array.size row)

theorem CompPoly.PolynomialMatrix.zeroRow_rowIsZero {F : Type u_1} [Field F] [BEq F] (width : ℕ) : RowIsZero (zeroRow width)

theorem CompPoly.PolynomialMatrix.rowScalePolynomial_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) : rowScalePolynomial 0 row = zeroRow (Array.size row)

theorem CompPoly.PolynomialMatrix.rowAdd_zeroRow_zeroRow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (width : ℕ) : rowAdd (zeroRow width) (zeroRow width) = zeroRow width

theorem CompPoly.PolynomialMatrix.rowAdd_zeroRow_right {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {width : ℕ} (row : PolynomialRow F) (hsize : Array.size row = width) : rowAdd row (zeroRow width) = row

theorem CompPoly.PolynomialMatrix.rowScalePolynomial_rowAdd {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c : CPolynomial F) (a b : PolynomialRow F) : rowScalePolynomial c (rowAdd a b) = rowAdd (rowScalePolynomial c a) (rowScalePolynomial c b)

theorem CompPoly.PolynomialMatrix.rowAdd_assoc {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (a b c : PolynomialRow F) : rowAdd (rowAdd a b) c = rowAdd a (rowAdd b c)

theorem CompPoly.PolynomialMatrix.rowAdd_rowNeg_left {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) : rowAdd (rowNeg row) row = zeroRow (Array.size row)

theorem CompPoly.PolynomialMatrix.rowSub_add_cancel {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {a b : PolynomialRow F} (hsize : Array.size b = Array.size a) : rowAdd (rowSub a b) b = a

theorem CompPoly.PolynomialMatrix.rowAdd_medial {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (a b c d : PolynomialRow F) : rowAdd (rowAdd a b) (rowAdd c d) = rowAdd (rowAdd a c) (rowAdd b d)

theorem CompPoly.PolynomialMatrix.rowScalePolynomial_add {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c d : CPolynomial F) (row : PolynomialRow F) : rowAdd (rowScalePolynomial c row) (rowScalePolynomial d row) = rowScalePolynomial (c + d) row

theorem CompPoly.PolynomialMatrix.rowScalePolynomial_assoc {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (c d : CPolynomial F) (row : PolynomialRow F) : rowScalePolynomial c (rowScalePolynomial d row) = rowScalePolynomial (c * d) row

theorem CompPoly.PolynomialMatrix.getD_map_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (coeffs : Array (CPolynomial F)) (c : CPolynomial F) (i : ℕ) : (Array.map (fun (q : CPolynomial F) => c * q) coeffs).getD i 0 = c * coeffs.getD i 0

theorem CompPoly.PolynomialMatrix.getD_ofFn_add {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (n : ℕ) (coeffsA coeffsB : Array (CPolynomial F)) {i : ℕ} (hi : i < n) : (Array.ofFn fun (k : Fin n) => coeffsA.getD (↑k) 0 + coeffsB.getD (↑k) 0).getD i 0 = coeffsA.getD i 0 + coeffsB.getD i 0

theorem CompPoly.PolynomialMatrix.rowAdd_rowLinearCombination_range {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (coeffsA coeffsB : Array (CPolynomial F)) (n : ℕ) : n ≤ Array.size M → rowAdd (List.foldl (fun (acc : PolynomialRow F) (i : ℕ) => rowAdd acc (rowScalePolynomial (coeffsA.getD i 0) (Array.getD M i #[]))) (zeroRow M.MatrixWidth) (List.range n)) (List.foldl (fun (acc : PolynomialRow F) (i : ℕ) => rowAdd acc (rowScalePolynomial (coeffsB.getD i 0) (Array.getD M i #[]))) (zeroRow M.MatrixWidth) (List.range n)) = List.foldl (fun (acc : PolynomialRow F) (i : ℕ) => rowAdd acc (rowScalePolynomial ((Array.ofFn fun (k : Fin (Array.size M)) => coeffsA.getD (↑k) 0 + coeffsB.getD (↑k) 0).getD i 0) (Array.getD M i #[]))) (zeroRow M.MatrixWidth) (List.range n)

theorem CompPoly.PolynomialMatrix.rowAdd_rowLinearCombination {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (coeffsA coeffsB : Array (CPolynomial F)) : rowAdd (rowLinearCombination coeffsA M) (rowLinearCombination coeffsB M) = rowLinearCombination (Array.ofFn fun (k : Fin (Array.size M)) => coeffsA.getD (↑k) 0 + coeffsB.getD (↑k) 0) M

theorem CompPoly.PolynomialMatrix.rowAdd_mem_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} {a b : PolynomialRow F} (ha : a ∈ M.RowSpan) (hb : b ∈ M.RowSpan) : rowAdd a b ∈ M.RowSpan

theorem CompPoly.PolynomialMatrix.C_neg_one_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (p : CPolynomial F) : CPolynomial.C (-1) * p = -p

theorem CompPoly.PolynomialMatrix.rowNeg_eq_rowScalePolynomial {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) : rowNeg row = rowScalePolynomial (CPolynomial.C (-1)) row

theorem CompPoly.PolynomialMatrix.rowScalePolynomial_rowLinearCombination_range {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (c : CPolynomial F) (coeffs : Array (CPolynomial F)) (n : ℕ) : rowScalePolynomial c (List.foldl (fun (acc : PolynomialRow F) (i : ℕ) => rowAdd acc (rowScalePolynomial (coeffs.getD i 0) (Array.getD M i #[]))) (zeroRow M.MatrixWidth) (List.range n)) = List.foldl (fun (acc : PolynomialRow F) (i : ℕ) => rowAdd acc (rowScalePolynomial ((Array.map (fun (q : CPolynomial F) => c * q) coeffs).getD i 0) (Array.getD M i #[]))) (zeroRow M.MatrixWidth) (List.range n)

theorem CompPoly.PolynomialMatrix.rowScalePolynomial_rowLinearCombination {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} (c : CPolynomial F) (coeffs : Array (CPolynomial F)) : rowScalePolynomial c (rowLinearCombination coeffs M) = rowLinearCombination (Array.map (fun (q : CPolynomial F) => c * q) coeffs) M

theorem CompPoly.PolynomialMatrix.rowScalePolynomial_mem_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} {row : PolynomialRow F} (c : CPolynomial F) (hrow : row ∈ M.RowSpan) : rowScalePolynomial c row ∈ M.RowSpan

theorem CompPoly.PolynomialMatrix.rowScaleMonomial_mem_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} {row : PolynomialRow F} (c : F) (d : ℕ) (hrow : row ∈ M.RowSpan) : rowScaleMonomial c d row ∈ M.RowSpan

theorem CompPoly.PolynomialMatrix.rowNeg_mem_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} {row : PolynomialRow F} (hrow : row ∈ M.RowSpan) : rowNeg row ∈ M.RowSpan

theorem CompPoly.PolynomialMatrix.rowSub_mem_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {M : PolynomialMatrix F} {a b : PolynomialRow F} (ha : a ∈ M.RowSpan) (hb : b ∈ M.RowSpan) : rowSub a b ∈ M.RowSpan

theorem CompPoly.PolynomialMatrix.cancelShiftedLeadingTerm_mem_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} {target reducer : PolynomialRow F} {shift : Array ℕ} (htarget : target ∈ M.RowSpan) (hreducer : reducer ∈ M.RowSpan) : cancelShiftedLeadingTerm target reducer shift ∈ M.RowSpan

theorem CompPoly.PolynomialMatrix.cancelShiftedLeadingTerm_target_mem_rowSpan {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} {target reducer : PolynomialRow F} {shift : Array ℕ} (hcancel : cancelShiftedLeadingTerm target reducer shift ∈ M.RowSpan) (hreducer : reducer ∈ M.RowSpan) (hsize : Array.size reducer = Array.size target) : target ∈ M.RowSpan

theorem CompPoly.PolynomialMatrix.cancelShiftedLeadingTerm_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {target reducer : PolynomialRow F} {shift : Array ℕ} (hsize : Array.size reducer = Array.size target) : Array.size (cancelShiftedLeadingTerm target reducer shift) = Array.size target