Documentation

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

The monad for the Gaussian Elimination algorithm.

Equations
Instances For
    source
    def Linarith.SimplexAlgorithm.Gauss.findNonzeroRow (row : Nat) (col : Nat) {n : Nat} {m : Nat} :
    Linarith.SimplexAlgorithm.Gauss.GaussM n m (Option Nat)

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Linarith.SimplexAlgorithm.Gauss.swapRows {n : Nat} {m : Nat} (i : Nat) (j : Nat) :
      Linarith.SimplexAlgorithm.Gauss.GaussM n m Unit

      Swaps two rows.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Linarith.SimplexAlgorithm.Gauss.subtractRow {n : Nat} {m : Nat} (i : Nat) (j : Nat) (coef : Rat) :
        Linarith.SimplexAlgorithm.Gauss.GaussM n m Unit

        Subtracts i-th row * coef from j-th row.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Linarith.SimplexAlgorithm.Gauss.divideRow {n : Nat} {m : Nat} (i : Nat) (coef : Rat) :
          Linarith.SimplexAlgorithm.Gauss.GaussM n m Unit

          Divides row by coef.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Linarith.SimplexAlgorithm.Gauss.getTableImp {n : Nat} {m : Nat} :
            Linarith.SimplexAlgorithm.Gauss.GaussM n m Linarith.SimplexAlgorithm.Table

            Implementation of getTable in GaussM monad.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Linarith.SimplexAlgorithm.Gauss.getTable {n : Nat} {m : Nat} (A : Linarith.SimplexAlgorithm.Matrix n m) :
              Linarith.SimplexAlgorithm.Table

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

              Equations
              Instances For