Nuprl Definition : matrix-ring
matrix-ring(r;n) == <Matrix(n;n;r), λu,v. ff, λu,v. ff, λM,N. M + N, 0, λM.-(M), λM,N. (M*N), I, λu,v. (inr ⋅ )>
Definitions occuring in Statement :
matrix-minus: -(M),
zero-matrix: 0,
identity-matrix: I,
matrix-times: (M*N),
matrix-plus: M + N,
matrix: Matrix(n;m;r),
bfalse: ff,
it: ⋅,
lambda: λx.A[x],
pair: <a, b>,
inr: inr x
Definitions occuring in definition :
matrix: Matrix(n;m;r),
bfalse: ff,
matrix-plus: M + N,
zero-matrix: 0,
matrix-minus: -(M),
matrix-times: (M*N),
pair: <a, b>,
identity-matrix: I,
lambda: λx.A[x],
inr: inr x ,
it: ⋅
FDL editor aliases :
matrix-ring
Latex:
matrix-ring(r;n) == <Matrix(n;n;r), \mlambda{}u,v. ff, \mlambda{}u,v. ff, \mlambda{}M,N. M + N, 0, \mlambda{}M.-(M), \mlambda{}M,N. (M*N), I, \mlambda{}u\000C,v. (inr \mcdot{} )>
Date html generated:
2018_05_21-PM-09_35_24
Last ObjectModification:
2017_12_11-PM-00_29_41
Theory : matrices
Home
Index