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.

Main definitions

• mkBareissDecomposition: produce and elaborate the decomposition of a matrix literal.
• BareissResult: the elaborated certificate together with the computed decomposition data.
• checkBareissApplicable: the applicability check of the Bareiss method.
• producerFor: select the computation model for a ring.

def Mathlib.Tactic.Echelon.checkBareissApplicable (R : Lean.Expr) : Lean.MetaM (Except Lean.MessageData Unit)

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.producerFor (R : Lean.Expr) : Lean.MetaM Producer

Select the computation model for the ring expression R: the first registered bareiss_ext extension that handles R, 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 producing a decomposition by Bareiss.

• cert : Lean.Expr

  The elaborated Echelon.Decomposition certificate term.

• data : BareissData Lean.Expr

  The decomposition data underlying the certificate.

def Mathlib.Tactic.Echelon.mkBareissDecomposition {u : Lean.Level} (A : Lean.Expr) (m n : ℕ) (α : Q(Type u)) (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.