# 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
@[reducible, inline]
abbrev Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.GaussM (n m : Nat) (matType : Nat → Nat → Type) (α : Type) :
Type

The monad for the Gaussian Elimination algorithm.

Equations

- Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.GaussM n m matType = StateT (matType n m) Lean.CoreM

Instances For

source
def Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.findNonzeroRow {n m : Nat} {matType : Nat → Nat → Type} [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

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

Instances For

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

Implementation of `getTableau` in `GaussM` monad.

Equations

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

Instances For

source
def Mathlib.Tactic.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.

Equations

- Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.getTableau A = do let __do_lift ← StateT.run Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.getTableauImp A pure __do_lift.fst

Instances For