Documentation

CompPoly.LinearAlgebra.PolynomialMatrix.RowSpan

Row Span for Polynomial Matrices #

source
def CompPoly.PolynomialMatrix.rowLinearCombination {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (coeffs : Array (CPolynomial F)) (M : PolynomialMatrix F) :
PolynomialRow F

Polynomial linear combination of matrix rows.

Instances For
    source
    def CompPoly.PolynomialMatrix.RowSpan {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (M : PolynomialMatrix F) :
    Set (PolynomialRow F)

    Row module generated by the matrix rows.

    Instances For
      source
      theorem CompPoly.PolynomialMatrix.matrix_row_mem_rowSpan {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} {row : PolynomialRow F} (hM : M.WellFormed) (hrow : row ∈ M.MatrixRows) :
      row ∈ M.RowSpan

      Every stored row belongs to its matrix row span.

      source
      def CompPoly.PolynomialMatrix.RowSpanEq {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (A B : PolynomialMatrix F) :
      Prop

      Row span extensional equality.

      Instances For