Determinants of matrix literals by echelon decomposition

proveEchelonDet evaluates the determinant of a square matrix literal with non-symbolic entries through the certificate Echelon.Decomposition A L σ pivot of its echelon decomposition.

Main definitions

• proveEchelonDet: proves A.det = v for a square matrix literal A from its echelon decomposition.
• detValue: computes the value of the determinant from the decomposition data.
• certifyDiagProd: computes the product of the diagonal of a list-based matrix literal with its proof.
• certifyPermSign: computes the sign of the row permutation from its swaps with its proof.

Implementation notes

The determinant is the quotient of the diagonal products of U and L, up to the sign of the row permutation. The model computes it in its carrier by exact division. Where the division is not exact, as under the rational model's row scaling, the value is the fraction of the two products in norm_num's normal form when possible.

def Mathlib.Tactic.Determinant.certifyDiagProdList {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (k c : ℕ) (rows : Q(List (List «$α»))) : Lean.MetaM ((e : Q(«$α»)) × Q(diagProd «$k» «$c» «$rows» = «$e»))

Compute diagProd k c rows with a proof of the equality.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Determinant.certifyDiagProdList rα k 0 rows = pure ⟨q(1), q(⋯)⟩

def Mathlib.Tactic.Determinant.certifyDiagProd {u : Lean.Level} {m : ℕ} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (M : Echelon.ListMatrixLit α m m) : Lean.MetaM ((e : Q(«$α»)) × have a := M.lit; Q(diagProd 0 «$m» «$a» = «$e»))

Compute the product diagProd 0 m M.lit of the diagonal of M with a proof of the equality.

Equations

• Mathlib.Tactic.Determinant.certifyDiagProd rα M = Mathlib.Tactic.Determinant.certifyDiagProdList rα 0 m M.lit

def Mathlib.Tactic.Determinant.certifyPermSign {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) {m : ℕ} (swaps : Q(List (Fin «$m» × Fin «$m»))) (k : ℕ) : (s : Q(«$α»)) × Q(↑↑(Equiv.Perm.sign (Echelon.permOfSwaps «$swaps»)) = «$s»)

Compute the sign of the permutation from the swaps with the corresponding proof.

Equations

• Mathlib.Tactic.Determinant.certifyPermSign rα swaps k = ⟨q((-1) ^ «$k»), q(⋯)⟩

def Mathlib.Tactic.Determinant.detValue {u : Lean.Level} {α : Q(Type u)} (m : ℕ) {V : Type} (model : Echelon.Model α V) (data : Echelon.BareissData V) : Lean.MetaM (Option Q(«$α»))

The value of the determinant read off the decomposition data, computed by s * u / l, where u and l are the diagonal products of U and L and s is the sign of the swaps.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Determinant.proveEchelonDet {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (iα : Q(IsDomain «$α»)) (m : ℕ) (A : Q(Matrix (Fin «$m») (Fin «$m») «$α»)) (entries : Array (Array Q(«$α»))) : Lean.MetaM (Option ((v : Q(«$α»)) × Q(«$A».det = «$v»)))

Construct the value v and a proof that A.det = v by computing the echelon decomposition.

Equations

• One or more equations did not get rendered due to their size.