Nuprl Definition : real-matrix-times
(A*B) == λx,y. Σ{(A x i) * (B i y) | 0≤i≤n - 1}
Definitions occuring in Statement :
rsum: Σ{x[k] | n≤k≤m},
rmul: a * b,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
rsum: Σ{x[k] | n≤k≤m},
subtract: n - m,
natural_number: $n,
rmul: a * b,
apply: f a
FDL editor aliases :
real-matrix-times
Latex:
(A*B) == \mlambda{}x,y. \mSigma{}\{(A x i) * (B i y) | 0\mleq{}i\mleq{}n - 1\}
Date html generated:
2019_10_30-AM-08_15_22
Last ObjectModification:
2019_09_18-PM-06_55_19
Theory : reals
Home
Index