Nuprl Definition : least-factor
least-factor(n) == mu(λi.(n rem i + 2 =z 0)) + 2
Definitions occuring in Statement :
mu: mu(f),
eq_int: (i =z j),
lambda: λx.A[x],
remainder: n rem m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
mu: mu(f),
lambda: λx.A[x],
eq_int: (i =z j),
remainder: n rem m,
add: n + m,
natural_number: $n
FDL editor aliases :
least-factor
Latex:
least-factor(n) == mu(\mlambda{}i.(n rem i + 2 =\msubz{} 0)) + 2
Date html generated:
2016_05_15-PM-04_03_48
Last ObjectModification:
2015_09_23-AM-07_46_21
Theory : general
Home
Index