Nuprl Definition : padic-ring
padic-ring(p) == <padic(p), λu,v. ff, λu,v. ff, λu,v. pa-add(p;u;v), 0(p), λu.pa-minus(p;u), λu,v. pa-mul(p;u;v), 1(p),\000C λu,v. (inr ⋅ )>
Definitions occuring in Statement :
pa-minus: pa-minus(p;x),
pa-add: pa-add(p;x;y),
pa-mul: pa-mul(p;x;y),
pa-int: k(p),
padic: padic(p),
bfalse: ff,
it: ⋅,
lambda: λx.A[x],
pair: <a, b>,
inr: inr x ,
natural_number: $n
Definitions occuring in definition :
padic: padic(p),
bfalse: ff,
pa-add: pa-add(p;x;y),
pa-mul: pa-mul(p;x;y),
pair: <a, b>,
pa-int: k(p),
natural_number: $n,
lambda: λx.A[x],
inr: inr x ,
it: ⋅
FDL editor aliases :
padic-ring
Latex:
padic-ring(p) ==
<padic(p)
, \mlambda{}u,v. ff
, \mlambda{}u,v. ff
, \mlambda{}u,v. pa-add(p;u;v)
, 0(p)
, \mlambda{}u.pa-minus(p;u)
, \mlambda{}u,v. pa-mul(p;u;v)
, 1(p)
, \mlambda{}u,v. (inr \mcdot{} )>
Date html generated:
2018_05_21-PM-03_27_37
Last ObjectModification:
2018_01_28-PM-07_24_22
Theory : rings_1
Home
Index