Nuprl Definition : real-det
|M| ==
r-list-sum(map(λf.let k = rprod(0;n - 1;i.M i (f i)) in
if permutation-sign(n;f)=1 then k else -(k);permutations-list(n)))
Definitions occuring in Statement :
r-list-sum: r-list-sum(L),
rprod: rprod(n;m;k.x[k]),
rminus: -(x),
permutation-sign: permutation-sign(n;f),
map: map(f;as),
let: let,
int_eq: if a=b then c else d,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n,
permutations-list: permutations-list(n)
Definitions occuring in definition :
r-list-sum: r-list-sum(L),
map: map(f;as),
lambda: λx.A[x],
let: let,
rprod: rprod(n;m;k.x[k]),
subtract: n - m,
apply: f a,
int_eq: if a=b then c else d,
permutation-sign: permutation-sign(n;f),
natural_number: $n,
rminus: -(x),
permutations-list: permutations-list(n)
FDL editor aliases :
real-det
Latex:
|M| ==
r-list-sum(map(\mlambda{}f.let k = rprod(0;n - 1;i.M i (f i)) in
if permutation-sign(n;f)=1 then k else -(k);permutations-list(n)))
Date html generated:
2019_10_30-AM-08_20_33
Last ObjectModification:
2019_09_18-PM-05_14_45
Theory : reals
Home
Index