Class SQUARE-MATRIX

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

Slots on this class:

Documentation:

Class of the matrices whose number of columns is equal to the number

of rows

Instance-Of: Class

Subclass-Of: Matrix

Domain-Of: Size

Superclass-Of:

Diagonal-matrix, Identity-matrix, Invertible-matrix, Orthogonal-matrix

---

Slots on instances of this class:

Column-Dimension:

Same-Slot-Values: Row-dimension

Equivalence Axioms:

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

Axioms:

(Matrix ?M)

Other Related Axioms:

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

(=> (Size $X $Y) (Square-Matrix $X))

(=> (= (Size ?M) ?N) (Square-Matrix ?M))

(<=> (Identity-Matrix ?Im)
     (And (Square-Matrix ?Im)
          (Forall (?I ?J)
                  (=> (Defined (Value ?Im ?I ?J))
                      (And (=> (= ?I ?J) (= (Value ?Im ?I ?J) 1))
                           (=> (/= ?I ?J)
                               (Zero-Element (Value ?Im ?I ?J))))))))

(<=> (Diagonal-Matrix ?M)
     (And (Matrix ?M)
          (Square-Matrix ?M)
          (Forall (?I ?J)
                  (=> (And (Defined (Value ?M ?I ?J)) (/= ?I ?J))
                      (Zero-Element (Value ?M ?I ?J))))))

(=> (And (Square-Matrix ?M))
    (= (Determinant ?M)
       (Cond ((= 1 (Size ?M)) (Value ?M 1 1))
             ((< 1 (Size ?M))
              (Summation (Lambda (?J)
                                 (* (Value ?M 1 ?J)
                                    (Cofactor ?M 1 ?J)))
                         1
                         (Size ?M))))))

(Nth-Domain Cofactor 1 Square-Matrix)

(=> (= (Cofactor ?M ?I ?J) ?Cof) (Square-Matrix ?M))

(<=> (Invertible-Matrix ?M)
     (And (Square-Matrix ?M)
          (Exists (?M-1)
                  (And (Square-Matrix ?M-1)
                       (Identity-Matrix (* ?M ?M-1))
                       (Identity-Matrix (* ?M-1 ?M))))))

(<=> (Invertible-Matrix ?M)
     (And (Square-Matrix ?M) (Not (Zero-Element (Determinant ?M)))))

(<=> (Orthogonal-Matrix ?M)
     (And (Square-Matrix ?M)
          (Same-Values ?M Transpose Matrix-Inverse)))