Nuprl Definition : int_mod_ring
Integers mod n ⌜ℤ_n⌝ form a "discrete" commutative ring.
We use the form defined by Paul Jackson. It is a dependent tuple
and includes an equality test, and ordering, and a division operator.
Since ⌜ℤ_n⌝ isn't ordered and isn't a field (unless n is prime)
we supply "dummy" operations ⌜λu,v. ff⌝ and ⌜λu,v. (inr ⋅ )⌝ for the
ordering and division.
The equality test ⌜λu,v. (u mod n =z v mod n)⌝ does provide decidable
equality, so this structure is a ⌜CDRng⌝ (see int_mod_ring_wf) ⋅
int_mod_ring(n) == <ℤ_n, λu,v. (u mod n =z v mod n), λu,v. ff, λu,v. (u + v), 0, λu.(-u), λu,v. (u * v), 1, λu,v. (inr \000C⋅ )>
Definitions occuring in Statement :
int_mod: ℤ_n,
modulus: a mod n,
eq_int: (i =z j),
bfalse: ff,
it: ⋅,
lambda: λx.A[x],
pair: <a, b>,
inr: inr x ,
multiply: n * m,
add: n + m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
int_mod: ℤ_n,
eq_int: (i =z j),
modulus: a mod n,
bfalse: ff,
add: n + m,
minus: -n,
multiply: n * m,
pair: <a, b>,
natural_number: $n,
lambda: λx.A[x],
inr: inr x ,
it: ⋅
FDL editor aliases :
int_mod_ring
Latex:
int\_mod\_ring(n) ==
<\mBbbZ{}\_n, \mlambda{}u,v. (u mod n =\msubz{} v mod n), \mlambda{}u,v. ff, \mlambda{}u,v. (u + v), 0, \mlambda{}u.(-u), \mlambda{}u,v. (u * v), 1, \mlambda{}u,v. (in\000Cr \mcdot{} )>
Date html generated:
2016_07_08-PM-05_18_00
Last ObjectModification:
2015_09_23-AM-08_20_18
Theory : general
Home
Index