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.

@[reducible, inline]
abbrev Linarith.SimplexAlgorithm.Gauss.GaussM (n m : Nat) (matType : NatNatType) (α : Type) :

The monad for the Gaussian Elimination algorithm.

Equations
    Instances For
      def Linarith.SimplexAlgorithm.Gauss.findNonzeroRow {n m : Nat} {matType : NatNatType} [UsableInSimplexAlgorithm matType] (rowStart col : Nat) :
      GaussM n m matType (Option Nat)

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

      Equations
        Instances For
          def Linarith.SimplexAlgorithm.Gauss.getTableauImp {n m : Nat} {matType : NatNatType} [UsableInSimplexAlgorithm matType] :
          GaussM n m matType (Tableau matType)

          Implementation of getTableau in GaussM monad.

          Equations
            Instances For
              def Linarith.SimplexAlgorithm.Gauss.getTableau {n m : Nat} {matType : NatNatType} [UsableInSimplexAlgorithm matType] (A : matType n m) :

              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.

              Equations
                Instances For