Documentation

CompPoly.LinearAlgebra.Dense.RowOps

Dense Row Operations #

Executable row operations and Gauss-Jordan reduction for row-major matrices.

source
structure CompPoly.DenseMatrix.RrefResult (F : Type u_2) [Zero F] :
Type u_2

Result of row reduction, retaining pivot columns in row order.

Instances For
    source
    def CompPoly.DenseMatrix.swapRows {F : Type u_1} [Zero F] (M : DenseMatrix F) (rowA rowB : ℕ) :
    DenseMatrix F

    Swap two rows.

    Instances For
      source
      def CompPoly.DenseMatrix.scaleRow {F : Type u_1} [Field F] (M : DenseMatrix F) (row : ℕ) (factor : F) :
      DenseMatrix F

      Scale one row by a field element.

      Instances For
        source
        def CompPoly.DenseMatrix.addScaledRow {F : Type u_1} [Field F] (M : DenseMatrix F) (target source : ℕ) (factor : F) :
        DenseMatrix F

        Add factor times source row to target row.

        Instances For
          source
          def CompPoly.DenseMatrix.findPivotRow {F : Type u_1} [Zero F] [BEq F] (M : DenseMatrix F) (startRow col : ℕ) :
          Option ℕ

          Find a pivot row at or below startRow in column col.

          Instances For
            source
            def CompPoly.DenseMatrix.normalizeAndEliminate {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) (pivotRow pivotCol : ℕ) :
            DenseMatrix F

            Normalize the pivot row and clear the pivot column in every other row.

            Instances For
              source
              def CompPoly.DenseMatrix.rrefLoop {F : Type u_1} [Field F] [BEq F] :
              ℕ → ℕ → ℕ → DenseMatrix F → Array ℕ → RrefResult F

              Fuel-bounded Gauss-Jordan reduction.

              Instances For
                source
                def CompPoly.DenseMatrix.rref {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) :
                RrefResult F

                Reduced row-echelon form with pivot-column metadata.

                Instances For