Reflection certificates for determinants of echelon decompositions

The diagonal product of a matrix given as a list of rows, with a bridge lemma to the product over Fin m of an ofLists matrix. The determinant of a matrix follows from these pieces of an echelon decomposition.

Main definitions

• diagProd: the product of the diagonal entries of a list of rows.

Main results

• prod_diag_ofLists: the product of the diagonal of ofLists m m rows is diagProd 0 m rows.
• det_eq_of_decomposition: the determinant of A from an echelon decomposition of A, the diagonal products of L and of the echelon form, and the sign of the row permutation.

Diagonal products

def Mathlib.Tactic.Determinant.diagProd {α : Type u_1} [Zero α] [One α] [Mul α] (k c : ℕ) (rows : List (List α)) : α

The product of the entries of rows at positions (i, k + i) for i < c. Missing entries are padded with 0.

Equations

• Mathlib.Tactic.Determinant.diagProd k 0 rows = 1
• Mathlib.Tactic.Determinant.diagProd k c_2.succ rows = (List.drop k (rows.headD [])).headD 0 * Mathlib.Tactic.Determinant.diagProd (k + 1) c_2 rows.tail

theorem Mathlib.Tactic.Determinant.diagProd_zero {α : Type u_1} [Zero α] [One α] [Mul α] (k : ℕ) (rows : List (List α)) : diagProd k 0 rows = 1

theorem Mathlib.Tactic.Determinant.diagProd_add_one_cons {α : Type u_1} [Zero α] [One α] [Mul α] {k c : ℕ} {row : List α} {rows : List (List α)} {d e : α} {suffix : List α} (hdrop : List.drop k row = d :: suffix) (h : diagProd (k + 1) c rows = e) : diagProd k (c + 1) (row :: rows) = d * e

theorem Mathlib.Tactic.Determinant.diagProd_eq {α : Type u_1} [CommMonoid α] [Zero α] (k c : ℕ) (rows : List (List α)) : diagProd k c rows = ∏ i : Fin c, (rows.getD ↑i []).getD (k + ↑i) 0

theorem Mathlib.Tactic.Determinant.prod_diag_ofLists {α : Type u_1} [CommMonoid α] [Zero α] (m : ℕ) (rows : List (List α)) : ∏ i : Fin m, Matrix.ofLists m m rows i i = diagProd 0 m rows

Determinants from echelon decompositions

theorem Mathlib.Tactic.Determinant.det_eq_of_decomposition {m : ℕ} {R : Type u_2} [CommRing R] [IsDomain R] {A : Matrix (Fin m) (Fin m) R} {rowsL rowsU : List (List R)} {σ : Equiv.Perm (Fin m)} {pivot : Fin m → WithTop (Fin m)} (cert : Echelon.Decomposition A (Matrix.ofLists m m rowsL) σ pivot) {l u s v : R} (hU : Matrix.ofLists m m rowsL * A.submatrix (⇑σ) id = Matrix.ofLists m m rowsU) (hl : diagProd 0 m rowsL = l) (hu : diagProd 0 m rowsU = u) (hs : ↑↑(Equiv.Perm.sign σ) = s) (hv : l * (s * v) = u) : A.det = v