Nuprl Definition : gen-divisors-sum

Σ i|n. f[i] ==  Σ(i∈[1, n + 1)). if (n rem i =z 0) then f[i] else 0 fi 


Definitions occuring in Statement :  bag-summation: Σ(x∈b). f[x],  from-upto: [n, m),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  remainder: n rem m,  add: n + m,  natural_number: $n,  rng_zero: 0,  rng_plus: +r
Definitions occuring in definition :  bag-summation: Σ(x∈b). f[x],  rng_plus: +r,  from-upto: [n, m),  add: n + m,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  remainder: n rem m,  natural_number: $n,  rng_zero: 0
FDL editor aliases :  gen-divisors-sum
Latex:
\mSigma{}  i|n.  f[i]  ==    \mSigma{}(i\mmember{}[1,  n  +  1)).  if  (n  rem  i  =\msubz{}  0)  then  f[i]  else  0  fi 


Date html generated: 2016_05_15-PM-04_22_15
Last ObjectModification: 2015_09_23-AM-07_48_00

Theory : general


Home Index