is an isometry where *U* is given, *U* is known
to be a unitary and *W* is a given.
Thus, we are
trying to solve the following collection of
equations
for *x*.

Now, of course, since is invertible,
*x* = 0. Let us see how NCProcess1 behaves on the equations
of (§).
NCProcess1 creates the following output which we
call a ``spreadsheet''.
The appearing
in the spreadsheet below may be read as equal sign.

| ||
---|---|---|

YOUR SESSION HAS DIGESTED | ||

THE FOLLOWING RELATIONS | ||

{

The corresponding rules are the following:

*x**
0

The expressions with unknown variables {}

and knowns {

*U** *U*
1

*W** *W*
1

USER CREATIONS APPEAR BELOW | ||
---|---|---|

SOME RELATIONS WHICH APPEAR BELOW | ||||
---|---|---|---|---|

MAY BE UNDIGESTED | ||||

{}

The polynomials listed in the spreadsheet
above
generated the same ideal as
(§). Therefore, any solution
to (§) is a solution of the
equations in the spreadsheet and vice-versa.
Therefore,
if *U* is unitary, then the matrix in
(§)
is an isometry if and only if *x* is the zero matrix and
*W* is an isometry.

Wed Jul 3 10:27:42 PDT 1996