Nuprl Definition : cross-product
(a x b) ==
  λi.[((a 1) * (b 2)) +r (-r ((a 2) * (b 1)));
      ((a 2) * (b 0)) +r (-r ((a 0) * (b 2)));
      ((a 0) * (b 1)) +r (-r ((a 1) * (b 0)))][i]
Definitions occuring in Statement : 
select: L[n]
, 
cons: [a / b]
, 
nil: []
, 
infix_ap: x f y
, 
apply: f a
, 
lambda: λx.A[x]
, 
natural_number: $n
, 
rng_times: *
, 
rng_minus: -r
, 
rng_plus: +r
Definitions occuring in definition : 
lambda: λx.A[x]
, 
select: L[n]
, 
cons: [a / b]
, 
rng_plus: +r
, 
rng_minus: -r
, 
infix_ap: x f y
, 
rng_times: *
, 
apply: f a
, 
natural_number: $n
, 
nil: []
FDL editor aliases : 
cross-product
Latex:
(a  x  b)  ==
    \mlambda{}i.[((a  1)  *  (b  2))  +r  (-r  ((a  2)  *  (b  1)));
            ((a  2)  *  (b  0))  +r  (-r  ((a  0)  *  (b  2)));
            ((a  0)  *  (b  1))  +r  (-r  ((a  1)  *  (b  0)))][i]
Date html generated:
2018_05_21-PM-09_40_53
Last ObjectModification:
2017_12_18-PM-01_24_41
Theory : matrices
Home
Index