Nuprl Definition : p2J
p2J(a;b) ==
  λi.if (i =z 0) then ((a 1) * (b 2)) - (b 1) * (a 2)
     if (i =z 1) then ((a 2) * (b 0)) - (b 2) * (a 0)
     else ((a 1) * (b 0)) - (b 1) * (a 0)
     fi 
Definitions occuring in Statement : 
rsub: x - y
, 
rmul: a * b
, 
ifthenelse: if b then t else f fi 
, 
eq_int: (i =z j)
, 
apply: f a
, 
lambda: λx.A[x]
, 
natural_number: $n
Definitions occuring in definition : 
lambda: λx.A[x]
, 
ifthenelse: if b then t else f fi 
, 
eq_int: (i =z j)
, 
rsub: x - y
, 
rmul: a * b
, 
apply: f a
, 
natural_number: $n
FDL editor aliases : 
p2J
Latex:
p2J(a;b)  ==
    \mlambda{}i.if  (i  =\msubz{}  0)  then  ((a  1)  *  (b  2))  -  (b  1)  *  (a  2)
          if  (i  =\msubz{}  1)  then  ((a  2)  *  (b  0))  -  (b  2)  *  (a  0)
          else  ((a  1)  *  (b  0))  -  (b  1)  *  (a  0)
          fi 
Date html generated:
2017_10_05-AM-00_20_07
Last ObjectModification:
2017_06_17-AM-10_09_32
Theory : inner!product!spaces
Home
Index