Function ROW-DIMENSION

• Defined in theory: Basic-matrix-algebra
• Source code: basic-matrix.lisp

Slots on this function:

Documentation:

The number of rows in a matrix.

Instance-Of: Function

Arity: 2

Domain: Matrix

Range: Positive-integer

Other Related Axioms:

(=> (And (Positive-Integer ?I)
         (Positive-Integer ?J)
         (=< ?I (Row-Dimension ?M))
         (=< ?J (Column-Dimension ?M)))
    (Defined (Value ?M ?I ?J)))

(Inherited-Facet-Value Slot-Cardinality Matrix Row-Dimension 1)

(Inherited-Facet-Value Slot-Value-Type
                       Matrix
                       Row-Dimension
                       Positive-Integer)

(<=> (Matrix ?M)
     (And (Function ?M)
          (= (Arity ?M) 3)
          (Value-Type ?M Row-Dimension Positive-Integer)
          (Value-Cardinality ?M Row-Dimension 1)
          (Value-Type ?M Column-Dimension Positive-Integer)
          (Value-Cardinality ?M Column-Dimension 1)
          (=> (And (Positive-Integer ?I)
                   (Positive-Integer ?J)
                   (=< ?I (Row-Dimension ?M))
                   (=< ?J (Column-Dimension ?M)))
              (Defined (Value ?M ?I ?J)))))

(=> (Row-Dimension $X $Y) (Positive-Integer $Y))

(=> (Row-Dimension $X $Y) (Matrix $X))

(<= (Row-Dimension $X 1) (Row-Matrix $X))

(<=> (Row-Matrix ?M) (And (Matrix ?M) (= (Row-Dimension ?M) 1)))

(=> (= (Matrix-Of-Rows @Elements) ?M)
    (= (Row-Dimension ?M) (Length (Listof @Elements))))

(=> (= (Matrix-Of-Columns @Elements) ?M)
    (=> (And (Item ?E1 (Listof @Elements))
             (Item ?E2 (Listof @Elements)))
        (= (Row-Dimension ?E1) (Row-Dimension ?E2))))

(=> (= (Transpose ?A) ?B)
    (= (Row-Dimension ?A) (Column-Dimension ?B)))

(=> (= (Transpose ?A) ?B)
    (= (Column-Dimension ?A) (Row-Dimension ?B)))

(=> (= (Row ?M ?I) ?L) (=< ?I (Row-Dimension ?M)))

(=> (= (Column ?M ?I) ?L) (= (Row-Dimension ?M) (Row-Dimension ?L)))

(Inherited-Facet-Value Same-Slot-Values
                       Square-Matrix
                       Column-Dimension
                       Row-Dimension)

(<=> (Square-Matrix ?M)
     (And (Matrix ?M)
          (Same-Values ?M Column-Dimension Row-Dimension)))

(=> (= (Size ?M) ?N) (= ?N (Row-Dimension ?M)))

(=> (And (Matrix ?A)
         (Matrix ?B)
         (= (Column-Dimension ?A) (Row-Dimension ?B)))
    (<=> (* ?A ?B ?C)
         (And (Matrix ?C)
              (= (Row-Dimension ?A) (Row-Dimension ?C))
              (= (Column-Dimension ?B) (Column-Dimension ?C))
              (Forall (?I ?J)
                      (=> (Defined (Value ?C ?I ?J))
                          (= (Value ?C ?I ?J)
                             (Summation (Lambda (?K)
                                                (* (Value ?A ?I ?K)
                                                   (Value ?B ?K ?J)))
                                        1
                                        (Column-Dimension ?A))))))))

(=> (And (Matrix ?A)
         (Matrix ?B)
         (= (Row-Dimension ?A) (Row-Dimension ?B))
         (= (Column-Dimension ?A) (Column-Dimension ?B)))
    (<=> (+ ?A ?B ?C)
         (And (Matrix ?C)
              (= (Row-Dimension ?A) (Row-Dimension ?C))
              (= (Column-Dimension ?A) (Column-Dimension ?C))
              (Forall (?I ?J)
                      (=> (Defined (Value ?C ?I ?J))
                          (= (Value ?C ?I ?J)
                             (+ (Value ?A ?I ?J) (Value ?B ?I ?J))))))))

(=> (And (Matrix ?A)
         (Matrix ?B)
         (= (Row-Dimension ?A) (Row-Dimension ?B))
         (= (Column-Dimension ?A) (Column-Dimension ?B)))
    (<=> (- ?A ?B ?C)
         (And (Matrix ?C)
              (= (Row-Dimension ?A) (Row-Dimension ?C))
              (= (Column-Dimension ?A) (Column-Dimension ?C))
              (Forall (?I ?J)
                      (=> (Defined (Value ?C ?I ?J))
                          (= (Value ?C ?I ?J)
                             (- (Value ?A ?I ?J) (Value ?B ?I ?J))))))))

(=> (= (Matrix-Less-Row-And-Column ?A ?I ?J) ?B)
    (= (Row-Dimension ?B) (- (Row-Dimension ?A) 1)))

(=> (= (Matrix-Less-Row ?A ?I) ?B)
    (= (Row-Dimension ?B) (- (Row-Dimension ?A) 1)))

(=> (= (Matrix-Less-Column ?A ?I) ?B)
    (= (Row-Dimension ?B) (Row-Dimension ?A)))