Nuprl Definition : determinant
determinant(n;r) ==
primrec(n;λm.1;λn',d,m. (Σ(r) 0 ≤ i < n' + 1. if isEven(i) then m[0,i] else -r m[0,i] fi * (d matrix-minor(0;i;m))))
Definitions occuring in Statement :
matrix-minor: matrix-minor(i;j;m),
matrix-ap: M[i,j],
isEven: isEven(n),
primrec: primrec(n;b;c),
ifthenelse: if b then t else f fi ,
infix_ap: x f y,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n,
rng_sum: rng_sum,
rng_one: 1,
rng_times: *,
rng_minus: -r
Definitions occuring in definition :
primrec: primrec(n;b;c),
rng_one: 1,
lambda: λx.A[x],
rng_sum: rng_sum,
add: n + m,
infix_ap: x f y,
rng_times: *,
ifthenelse: if b then t else f fi ,
isEven: isEven(n),
rng_minus: -r,
matrix-ap: M[i,j],
apply: f a,
matrix-minor: matrix-minor(i;j;m),
natural_number: $n
FDL editor aliases :
determinant
Latex:
determinant(n;r) ==
primrec(n;\mlambda{}m.1;\mlambda{}n',d,m. (\mSigma{}(r) 0
\mleq{} i
< n' + 1
if isEven(i) then m[0,i] else -r m[0,i] fi * (d matrix-minor(0;i;m))))
Date html generated:
2018_05_21-PM-09_37_43
Last ObjectModification:
2017_12_12-AM-10_22_43
Theory : matrices
Home
Index