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

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

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

theorem HexMatrixTheory.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 HexMatrixTheory.swapRows_length (a b : ℕ) (A : List (List ℤ)) : (Hex.Matrix.DetWitness.swapRows a b A).length = A.length

theorem HexMatrixTheory.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 HexMatrixTheory.applySwaps_length (s : List (ℕ × ℕ)) (A : List (List ℤ)) : (Hex.Matrix.DetWitness.applySwaps s A).length = A.length

theorem HexMatrixTheory.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 HexMatrixTheory.signOf_eq (s : List (ℕ × ℕ)) : Hex.Matrix.DetWitness.signOf s = (-1) ^ s.length

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

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

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

theorem HexMatrixTheory.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.Packed.dotInt (ts.getD k []) c = 0) ∧ ∀ k' < k, Hex.Matrix.Packed.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.Packed.dotInt (ts.getD ↑k []) (cs.getD ↑k [])).prod

theorem HexMatrixTheory.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 HexMatrixTheory.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 HexMatrixTheory.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 HexMatrixTheory.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 HexMatrixTheory.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 HexMatrixTheory.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 HexMatrixTheory.prodNat_cast (s : List ℕ) (r : ℕ) (hs : s.length = r) : ↑(Hex.Matrix.DetWitness.prodNat s) = ∏ i : Fin r, ↑(s.getD (↑i) 1)

theorem HexMatrixTheory.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 HexMatrixTheory.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.

theorem HexMatrixTheory.mem_nthRow (A : List (List ℤ)) (i : ℕ) : Hex.Matrix.DetWitness.nthRow A i ∈ A ∨ Hex.Matrix.DetWitness.nthRow A i = []

theorem HexMatrixTheory.mem_replaceRow (A : List (List ℤ)) (i : ℕ) (r x : List ℤ) (hx : x ∈ Hex.Matrix.DetWitness.replaceRow A i r) : x ∈ A ∨ x = r

theorem HexMatrixTheory.mem_swapRows (a b : ℕ) (A : List (List ℤ)) (x : List ℤ) (hx : x ∈ Hex.Matrix.DetWitness.swapRows a b A) : x ∈ A ∨ x = []

theorem HexMatrixTheory.mem_applySwaps (s : List (ℕ × ℕ)) (A : List (List ℤ)) (x : List ℤ) (hx : x ∈ Hex.Matrix.DetWitness.applySwaps s A) : x ∈ A ∨ x = []

theorem HexMatrixTheory.zeroDotsPacked_eq (W r k : ℕ) (hW : r * (k * k) < 2 ^ W) (t : List ℤ) (ht : ∀ x ∈ t, x.natAbs < k) (cs : List (List ℤ)) (hcs : ∀ c ∈ cs, c.length = r ∧ ∀ x ∈ c, x.natAbs < k) : Hex.Matrix.DetWitness.zeroDotsPacked W r (Hex.Matrix.Packed.packSignedCut W r t) (Hex.Matrix.Packed.packSignedCols W r cs) = Hex.Matrix.DetWitness.zeroDots t cs

theorem HexMatrixTheory.triangularCheckPacked_eq (W r k : ℕ) (hW : r * (k * k) < 2 ^ W) (d : ℤ) (done : List (List ℤ)) (i : ℕ) (ts cs : List (List ℤ)) (pl pu : ℤ) : (∀ c ∈ done, c.length = r ∧ ∀ x ∈ c, x.natAbs < k) → (∀ t ∈ ts, ∀ x ∈ t, x.natAbs < k) → (∀ c ∈ cs, c.length = r ∧ ∀ x ∈ c, x.natAbs < k) → Hex.Matrix.DetWitness.triangularCheckPacked W r d (Hex.Matrix.Packed.packSignedCols W r done) i ts (Hex.Matrix.Packed.packSignedRows W r ts) (Hex.Matrix.Packed.packSignedCols W r cs) pl pu = Hex.Matrix.DetWitness.triangularCheck d done i ts cs pl pu

theorem HexMatrixTheory.checkDetList_of_packed (W k n : ℕ) (L : List (List ℤ)) (c : Hex.Matrix.DetWitness) (h : Hex.Matrix.checkDetListPacked W k n L c = true) : Hex.Matrix.checkDetList n L c = true

A passing packed check is a passing plain check.

theorem HexMatrixTheory.det_eq_of_checkListPacked' {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (L : List (List ℤ)) (c : Hex.Matrix.DetWitness) (W k : ℕ) (hA : A = ofLists n n L) (h : Hex.Matrix.checkDetListPacked W k n L c = true) : A.det = c.value

theorem HexMatrixTheory.checkDetRat_of_packed (W k n : ℕ) (A : List (List ℚ)) (s : List ℕ) (B : List (List ℤ)) (c : Hex.Matrix.DetWitness) (v : ℚ) (h : Hex.Matrix.checkDetRatPacked W k n A s B c v = true) : Hex.Matrix.checkDetRat n A s B c v = true

theorem HexMatrixTheory.det_eq_of_checkRatPacked' {n : ℕ} (A : Matrix (Fin n) (Fin n) ℚ) (L : List (List ℚ)) (s : List ℕ) (B : List (List ℤ)) (c : Hex.Matrix.DetWitness) (v : ℚ) (W k : ℕ) (hA : A = ofLists n n L) (h : Hex.Matrix.checkDetRatPacked W k n L s B c v = true) : A.det = v