Documentation

Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss

Gaussian Elimination algorithm #

The first step of Linarith.SimplexAlgorithm.findPositiveVector is finding initial feasible solution which is done by standard Gaussian Elimination algorithm implemented in this file.

source
🔸 coverage
@[reducible, inline]
abbrev Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.GaussM (n m : ℕ) (matType : ℕ → ℕ → Type) (α : Type) :
Type

The monad for the Gaussian Elimination algorithm.

Instances For
    source
    🔸 coverage
    def Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.findNonzeroRow {n m : ℕ} {matType : ℕ → ℕ → Type} [UsableInSimplexAlgorithm matType] (rowStart col : ℕ) :
    GaussM n m matType (Option â„•)

    Finds the first row starting from the rowStart with nonzero element in the column col.

    Instances For
      source
      🔸 coverage
      def Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.getTableauImp {n m : ℕ} {matType : ℕ → ℕ → Type} [UsableInSimplexAlgorithm matType] :
      GaussM n m matType (Tableau matType)

      Implementation of getTableau in GaussM monad.

      Instances For
        source
        🔸 coverage
        def Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.getTableau {n m : ℕ} {matType : ℕ → ℕ → Type} [UsableInSimplexAlgorithm matType] (A : matType n m) :
        Lean.CoreM (Tableau matType)

        Given matrix A, solves the linear equation A x = 0 and returns the solution as a tableau where some variables are free and others (basic) variable are expressed as linear combinations of the free ones.

        Instances For