Nuprl Definition : Legendre-root

Legendre-root(n;i) ==
  primrec(n;λi.r0;λi,x. if i + 1=1
                        then λi.r0
                        else (λi@0.rational_fun_zero(λx.ratLegendre(i + 1;x);if i@0=0

                                                                             then r(-1)

                                                                             else (x (i@0 - 1));if i@0=(i + 1) - 1

                                                                                                then r1

                                                                                                else (x i@0))))

i

Definitions occuring in Statement : ratLegendre: ratLegendre(n;x), rational_fun_zero: rational_fun_zero(f;a;b), int-to-real: r(n), primrec: primrec(n;b;c), int_eq: if a=b then c else d, apply: f a, lambda: λx.A[x], subtract: n - m, add: n + m, minus: -n, natural_number: $n
Definitions occuring in definition : primrec: primrec(n;b;c), rational_fun_zero: rational_fun_zero(f;a;b), lambda: λx.A[x], ratLegendre: ratLegendre(n;x), minus: -n, int_eq: if a=b then c else d, subtract: n - m, add: n + m, int-to-real: r(n), natural_number: $n, apply: f a
FDL editor aliases : Legendre-root

Latex:
Legendre-root(n;i) == primrec(n;\mlambda{}i.r0;\mlambda{}i,x. if i + 1=1 then \mlambda{}i.r0 else (\mlambda{}i@0.rational\_fun\_zero(\mlambda{}x.ratLegendre(i + 1;x);if i@0=0 then r(-1) else (x (i@0 - 1));if i@0=(i + 1) - 1 then r1 else (x i@0)))) i Date html generated: 2019_10_31-AM-06_19_49 Last ObjectModification: 2019_01_18-PM-06_05_27 Theory : reals_2 Home Index