The Bareiss decomposition driver

Given a matrix literal A over a commutative domain, the entry point mkBareissDecomposition selects a computation model for the element type, runs the elimination, and elaborates a certificate ⟨L, σ, pivot, …⟩ : Echelon.Decomposition A, with the certificate conditions checked by the kernel via decide. The elimination itself is the model-parameterized bareissDecomp in Mathlib.Tactic.Echelon.Core, and the certificate construction mkCertificate in Mathlib.Tactic.Echelon.Cert.

def Mathlib.Tactic.Echelon.checkBareissApplicable {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 with kernel-decidable equality.

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 : Type

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

• cert : Lean.Expr

  The elaborated Echelon.Decomposition certificate term.

• 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 Lean.Expr)) : Lean.MetaM BareissResult

Produce and elaborate the Echelon.Decomposition certificate of the matrix literal A.

Equations

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