Documentation

CompPoly.LinearAlgebra.PolynomialMatrix.Degree

Degree Helpers for Polynomial Rows #

source
def CompPoly.PolynomialMatrix.polynomialDegree? {F : Type u_1} [Zero F] [BEq F] (p : CPolynomial F) :
Option ℕ

Optional degree of a univariate polynomial, with none for zero.

Instances For
    source
    def CompPoly.PolynomialMatrix.RowIsZero {F : Type u_1} [Zero F] [BEq F] (row : PolynomialRow F) :
    Prop

    A row is zero when all entries are zero.

    Instances For
      source
      def CompPoly.PolynomialMatrix.rowIsZero {F : Type u_1} [Zero F] [BEq F] (row : PolynomialRow F) :
      Bool

      Executable zero-row predicate.

      Instances For
        source
        theorem CompPoly.PolynomialMatrix.rowIsZero_iff {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] {row : PolynomialRow F} :
        rowIsZero row = true ↔ RowIsZero row

        Boolean and propositional zero-row predicates agree.

        source
        theorem CompPoly.PolynomialMatrix.exists_nonzero_entry_of_rowIsZero_false {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] {row : PolynomialRow F} (hrow : rowIsZero row = false) :
        ∃ j < Array.size row, Array.getD row j 0 ≠ 0

        Nonzero rows have an indexed nonzero entry.