Nuprl Definition : padic
padic(p) == n:ℕ × if (n =z 0) then p-adics(p) else p-units(p) fi
Definitions occuring in Statement :
p-units: p-units(p),
p-adics: p-adics(p),
nat: ℕ,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
product: x:A × B[x],
natural_number: $n
Definitions occuring in definition :
product: x:A × B[x],
nat: ℕ,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n,
p-adics: p-adics(p),
p-units: p-units(p)
FDL editor aliases :
padic
Latex:
padic(p) == n:\mBbbN{} \mtimes{} if (n =\msubz{} 0) then p-adics(p) else p-units(p) fi
Date html generated:
2018_05_21-PM-03_25_54
Last ObjectModification:
2018_02_01-AM-10_49_26
Theory : rings_1
Home
Index