Class IDENTITY-MATRIX

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

Slots on this class:

Documentation:

Identity matrix is a class because it is not unique (one per size)

it is a matrix with only 1 on the diagonal and 0 everywhere else

Instance-Of: Class

Subclass-Of: Square-matrix

Equivalence Axioms:

(<=> (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))))))))

Axioms:

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

(Square-Matrix ?Im)

Other Related Axioms:

(<=> (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))))))))

(<=> (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))))))

(=> (= (Matrix-Inverse ?M) ?M-1) (Identity-Matrix (* ?M-1 ?M)))

(=> (= (Matrix-Inverse ?M) ?M-1) (Identity-Matrix (* ?M ?M-1)))