Nuprl Definition : int_pi_det_fun
(i)ℤ-det-fun == λj.(if (i =z 0) then j else j rem i fi =z 0)
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
lambda: λx.A[x],
remainder: n rem m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
remainder: n rem m,
natural_number: $n
Latex:
(i)\mBbbZ{}-det-fun == \mlambda{}j.(if (i =\msubz{} 0) then j else j rem i fi =\msubz{} 0)
Date html generated:
2016_05_15-PM-00_25_45
Last ObjectModification:
2015_09_23-AM-06_26_06
Theory : rings_1
Home
Index