Nuprl Definition : p-adic-ring
ℤ(p) == <p-adics(p), λu,v. ff, λu,v. ff, λu,v. u + v, 0(p), λu.-(u), λu,v. u * v, 1(p), λu,v. (inr ⋅ )>
Definitions occuring in Statement :
p-int: k(p),
p-minus: -(x),
p-mul: x * y,
p-add: x + y,
p-adics: p-adics(p),
bfalse: ff,
it: ⋅,
lambda: λx.A[x],
pair: <a, b>,
inr: inr x ,
natural_number: $n
Definitions occuring in definition :
p-adics: p-adics(p),
bfalse: ff,
p-add: x + y,
p-minus: -(x),
p-mul: x * y,
pair: <a, b>,
p-int: k(p),
natural_number: $n,
lambda: λx.A[x],
inr: inr x ,
it: ⋅
FDL editor aliases :
p-adic-ring
Latex:
\mBbbZ{}(p) == <p-adics(p), \mlambda{}u,v. ff, \mlambda{}u,v. ff, \mlambda{}u,v. u + v, 0(p), \mlambda{}u.-(u), \mlambda{}u,v. u * v, 1(p), \mlambda{}u,v. (inr \000C\mcdot{} )>
Date html generated:
2018_05_21-PM-03_20_42
Last ObjectModification:
2018_01_27-AM-11_49_48
Theory : rings_1
Home
Index