Nuprl Definition : p-adics
p-adics(p) == {f:n:ℕ+ ⟶ ℕp^n| ∀n:ℕ+. ((f (n + 1)) ≡ (f n) mod p^n)}
Definitions occuring in Statement :
eqmod: a ≡ b mod m,
exp: i^n,
int_seg: {i..j-},
nat_plus: ℕ+,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
int_seg: {i..j-},
all: ∀x:A. B[x],
nat_plus: ℕ+,
eqmod: a ≡ b mod m,
exp: i^n,
add: n + m,
natural_number: $n,
apply: f a
FDL editor aliases :
p-adics
Latex:
p-adics(p) == \{f:n:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbN{}p\^{}n| \mforall{}n:\mBbbN{}\msupplus{}. ((f (n + 1)) \mequiv{} (f n) mod p\^{}n)\}
Date html generated:
2018_05_21-PM-03_17_41
Last ObjectModification:
2018_01_27-PM-00_37_59
Theory : rings_1
Home
Index