Nuprl Definition : int

Nuprl Definition : int_ring

ℤ-rng ==

  <ℤ, λu,v. (u =_z v), λu,v. u ≤z v, λu,v. (u + v), 0, λu.(-u), λu,v. (u * v), 1, λu,v. if (v =_z 0) then inr ⋅  else inl \000C(u ÷ v) fi >

Definitions occuring in Statement : le_int: i ≤z j, ifthenelse: if b then t else f fi , eq_int: (i =_z j), it: ⋅, lambda: λx.A[x], pair: <a, b>, inr: inr x , inl: inl x, divide: n ÷ m, multiply: n * m, add: n + m, minus: -n, natural_number: $n, int: ℤ
Definitions occuring in definition : int: ℤ, le_int: i ≤z j, add: n + m, minus: -n, multiply: n * m, pair: <a, b>, lambda: λx.A[x], ifthenelse: if b then t else f fi , eq_int: (i =_z j), natural_number: $n, inr: inr x , it: ⋅, inl: inl x, divide: n ÷ m

Latex:
\mBbbZ{}-rng == <\mBbbZ{} , \mlambda{}u,v. (u =\msubz{} v) , \mlambda{}u,v. u \mleq{}z v , \mlambda{}u,v. (u + v) , 0 , \mlambda{}u.(-u) , \mlambda{}u,v. (u * v) , 1 , \mlambda{}u,v. if (v =\msubz{} 0) then inr \mcdot{} else inl (u \mdiv{} v) fi > Date html generated: 2016_05_15-PM-00_25_37 Last ObjectModification: 2015_09_23-AM-06_26_05 Theory : rings_1 Home Index