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.
def
Linarith.SimplexAlgorithm.Gauss.getTableauImp
{n m : Nat}
{matType : Nat → Nat → Type}
[UsableInSimplexAlgorithm matType]
:
Implementation of getTableau
in GaussM
monad.
Equations
Instances For
def
Linarith.SimplexAlgorithm.Gauss.getTableau
{n m : Nat}
{matType : Nat → Nat → 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.