Documentation

CompPoly.LinearAlgebra.Dense.Kernel

Dense Homogeneous Kernels #

Executable homogeneous-kernel basis and witness extraction from row-reduced dense matrices.

source
def CompPoly.DenseMatrix.containsNat (xs : Array ℕ) (x : ℕ) :
Bool

Boolean membership test for natural-number arrays.

Instances For
    source
    def CompPoly.DenseMatrix.freeColumns (cols : ℕ) (pivots : Array ℕ) :
    Array ℕ

    Free columns of a row-reduced matrix.

    Instances For
      source
      def CompPoly.DenseMatrix.pivotRowOfColumn? (pivots : Array ℕ) (col : ℕ) :
      Option ℕ

      Pivot row for a pivot column, if the column is a pivot.

      Instances For
        source
        def CompPoly.DenseMatrix.basisVectorForFreeColumn {F : Type u_1} [Field F] [BEq F] (A : DenseMatrix F) (pivots : Array ℕ) (free : ℕ) :
        Array F

        Kernel basis vector corresponding to one free column of an RREF matrix.

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

          Homogeneous kernel basis extracted from the RREF free columns.

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

            One nonzero homogeneous-kernel witness, if a free column exists.

            Instances For