theorem HexMatrixMathlib.nthRow_eq_getD (A : List (List ℤ)) (i : ℕ) : Hex.Matrix.DetWitness.nthRow A i = A.getD i []

theorem HexMatrixMathlib.nthInt_eq_getD (a : List ℤ) (j : ℕ) : Hex.Matrix.DetWitness.nthInt a j = a.getD j 0

theorem HexMatrixMathlib.replaceRow_length (A : List (List ℤ)) (i : ℕ) (r : List ℤ) : (Hex.Matrix.DetWitness.replaceRow A i r).length = A.length

theorem HexMatrixMathlib.replaceRow_getD (A : List (List ℤ)) (i : ℕ) (r : List ℤ) (k : ℕ) (hi : i < A.length) : (Hex.Matrix.DetWitness.replaceRow A i r).getD k [] = if k = i then r else A.getD k []

theorem HexMatrixMathlib.swapRows_length (a b : ℕ) (A : List (List ℤ)) : (Hex.Matrix.DetWitness.swapRows a b A).length = A.length

theorem HexMatrixMathlib.swapRows_getD (a b : ℕ) (A : List (List ℤ)) (ha : a < A.length) (hb : b < A.length) (k : ℕ) : (Hex.Matrix.DetWitness.swapRows a b A).getD k [] = A.getD (if k = a then b else if k = b then a else k) []

theorem HexMatrixMathlib.applySwaps_length (s : List (ℕ × ℕ)) (A : List (List ℤ)) : (Hex.Matrix.DetWitness.applySwaps s A).length = A.length

theorem HexMatrixMathlib.swapsOk_cons (n a b : ℕ) (s : List (ℕ × ℕ)) (h : Hex.Matrix.DetWitness.swapsOk n ((a, b) :: s) = true) : a < n ∧ b < n ∧ a ≠ b ∧ Hex.Matrix.DetWitness.swapsOk n s = true

theorem HexMatrixMathlib.signOf_eq (s : List (ℕ × ℕ)) : Hex.Matrix.DetWitness.signOf s = (-1) ^ s.length

theorem HexMatrixMathlib.rowsLen_iff (m : ℕ) (L : List (List ℤ)) : Hex.Matrix.DetWitness.rowsLen m L = true ↔ ∀ r ∈ L, r.length = m

theorem HexMatrixMathlib.dotInt_eq_sum (a b : List ℤ) (r : ℕ) (h : a.length ≤ r) : Hex.Matrix.DetWitness.dotInt a b = ∑ k : Fin r, a.getD (↑k) 0 * b.getD (↑k) 0

theorem HexMatrixMathlib.column_length (j : ℕ) (A : List (List ℤ)) : (Hex.Matrix.DetWitness.column j A).length = A.length

theorem HexMatrixMathlib.column_getD (j : ℕ) (A : List (List ℤ)) (k : ℕ) : (Hex.Matrix.DetWitness.column j A).getD k 0 = (A.getD k []).getD j 0

theorem HexMatrixMathlib.columnsFrom_length (A : List (List ℤ)) (j k : ℕ) : (Hex.Matrix.DetWitness.columnsFrom A j k).length = k

theorem HexMatrixMathlib.columnsFrom_getD (A : List (List ℤ)) (j k l : ℕ) (hl : l < k) : (Hex.Matrix.DetWitness.columnsFrom A j k).getD l [] = Hex.Matrix.DetWitness.column (j + l) A

theorem HexMatrixMathlib.columns_length (m : ℕ) (A : List (List ℤ)) : (Hex.Matrix.DetWitness.columns m A).length = m

theorem HexMatrixMathlib.columns_getD (m : ℕ) (A : List (List ℤ)) (l : ℕ) (hl : l < m) : (Hex.Matrix.DetWitness.columns m A).getD l [] = Hex.Matrix.DetWitness.column l A

theorem HexMatrixMathlib.zeroDots_iff (t : List ℤ) (cs : List (List ℤ)) : Hex.Matrix.DetWitness.zeroDots t cs = true ↔ ∀ c ∈ cs, Hex.Matrix.DetWitness.dotInt t c = 0

theorem HexMatrixMathlib.anyNonzero_iff (v : List ℤ) : Hex.Matrix.DetWitness.anyNonzero v = true ↔ ∃ a ∈ v, a ≠ 0

theorem HexMatrixMathlib.triangularCheck_spec (d : ℤ) (done : List (List ℤ)) (i : ℕ) (ts cs : List (List ℤ)) (pl pu : ℤ) : Hex.Matrix.DetWitness.triangularCheck d done i ts cs pl pu = true → ts.length = cs.length ∧ (∀ k < ts.length, (ts.getD k []).length = i + k + 1 ∧ Hex.Matrix.DetWitness.nthInt (ts.getD k []) (i + k) ≠ 0 ∧ (∀ c ∈ done, Hex.Matrix.DetWitness.dotInt (ts.getD k []) c = 0) ∧ ∀ k' < k, Hex.Matrix.DetWitness.dotInt (ts.getD k []) (cs.getD k' []) = 0) ∧ pl * (List.ofFn fun (k : Fin ts.length) => Hex.Matrix.DetWitness.nthInt (ts.getD ↑k []) (i + ↑k)).prod * d = pu * (List.ofFn fun (k : Fin ts.length) => Hex.Matrix.DetWitness.dotInt (ts.getD ↑k []) (cs.getD ↑k [])).prod

theorem HexMatrixMathlib.ofLists_swapRows (n : ℕ) (L : List (List ℤ)) (hL : L.length = n) (a b : Fin n) : ofLists n n (Hex.Matrix.DetWitness.swapRows (↑a) (↑b) L) = (ofLists n n L).submatrix (⇑(Equiv.swap a b)) id

theorem HexMatrixMathlib.det_ofLists_applySwaps (n : ℕ) (s : List (ℕ × ℕ)) (L : List (List ℤ)) (hL : L.length = n) (hs : Hex.Matrix.DetWitness.swapsOk n s = true) : (ofLists n n (Hex.Matrix.DetWitness.applySwaps s L)).det = Hex.Matrix.DetWitness.signOf s * (ofLists n n L).det

theorem HexMatrixMathlib.det_eq_of_checkList (n : ℕ) (L : List (List ℤ)) (c : Hex.Matrix.DetWitness) (h : Hex.Matrix.checkDetList n L c = true) : (ofLists n n L).det = c.value

A passing kernel check determines the determinant of the row list's matrix.

theorem HexMatrixMathlib.det_eq_of_checkList' {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (L : List (List ℤ)) (c : Hex.Matrix.DetWitness) (hA : A = ofLists n n L) (h : Hex.Matrix.checkDetList n L c = true) : A.det = c.value

det_eq_of_checkList for a matrix identified with its row list; the tactic supplies hA by rfl for a vector chain.

theorem HexMatrixMathlib.scaledRow_spec (k : ℕ) (q : List ℚ) (b : List ℤ) (h : Hex.Matrix.DetWitness.scaledRow k q b = true) (j : ℕ) : ↑k * q.getD j 0 = ↑(b.getD j 0)

theorem HexMatrixMathlib.scaledRows_spec (s : List ℕ) (A : List (List ℚ)) (B : List (List ℤ)) (h : Hex.Matrix.DetWitness.scaledRows s A B = true) (i : ℕ) : 0 < s.getD i 1 ∧ ∀ (j : ℕ), ↑(s.getD i 1) * (A.getD i []).getD j 0 = ↑((B.getD i []).getD j 0)

theorem HexMatrixMathlib.prodNat_cast (s : List ℕ) (r : ℕ) (hs : s.length = r) : ↑(Hex.Matrix.DetWitness.prodNat s) = ∏ i : Fin r, ↑(s.getD (↑i) 1)

theorem HexMatrixMathlib.det_eq_of_checkRat (n : ℕ) (A : List (List ℚ)) (s : List ℕ) (B : List (List ℤ)) (c : Hex.Matrix.DetWitness) (v : ℚ) (h : Hex.Matrix.checkDetRat n A s B c v = true) : (ofLists n n A).det = v

A passing rational check determines the determinant of the rational row list's matrix.

theorem HexMatrixMathlib.det_eq_of_checkRat' {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) (L : List (List ℚ)) (s : List ℕ) (B : List (List ℤ)) (c : Hex.Matrix.DetWitness) (v : ℚ) (hA : A = ofLists n n L) (h : Hex.Matrix.checkDetRat n L s B c v = true) : A.det = v

det_eq_of_checkRat for a matrix identified with its row list.