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