The Bareiss decomposition driver

The entry point of the Bareiss decomposition of a matrix literal over a commutative domain. The elimination is the model-parameterized bareissDecomp in Mathlib.Tactic.Echelon.Core, and the certificate construction certifyDecomposition in Mathlib.Tactic.Echelon.Cert.

Main definitions

• mkBareissDecomposition: selects a model, runs the elimination algorithm and builds the certificate.
• BareissResult: the elaborated certificate together with the model and the raw decomposition data.
• modelFor: selects the computation model for a given ring.

def Mathlib.Tactic.Echelon.inferBareissRing {u : Lean.Level} (α : Q(Type u)) : Lean.MetaM (Except Lean.MessageData Q(CommRing «$α»))

The applicability check of the Bareiss method, which requires a commutative domain. It returns the commutative ring instance for the downstream functions to use.

Equations

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

def Mathlib.Tactic.Echelon.modelFor {u : Lean.Level} (α : Q(Type u)) (rα : Q(CommRing «$α»)) : Lean.MetaM ((c : Carrier) × Model α c.type)

Select the first registered computation model for the element type α, or the default rational model.

Equations

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

structure Mathlib.Tactic.Echelon.BareissResult {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (A : Q(Matrix (Fin «$m») (Fin «$n») «$α»)) : Type

The result of producer evaluation and certificate construction, together with the computation model.

• cert : DecompositionCert rα A

  The decomposition certificate with its reusable intermediate certificates.

• carrier : Carrier

  The carrier of the computation model.

• model : Model α self.carrier.type

  The computation model that produced the decomposition.

• data : BareissData self.carrier.type

  The decomposition data underlying the certificate, on the model's carrier.

def Mathlib.Tactic.Echelon.mkBareissDecomposition {u : Lean.Level} {m n : ℕ} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (A : Q(Matrix (Fin «$m») (Fin «$n») «$α»)) (entries : Array (Array Q(«$α»))) : Lean.MetaM (BareissResult rα A)

Produce the decomposition of the matrix literal A and elaborate its certificates.

Equations

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