Step
*
of Lemma
p-shift-0
No Annotations
∀p,n:ℕ+.  (p-shift(p;0(p);n) = 0(p) ∈ p-adics(p))
BY
{ (Intros THEN RWO "equal-p-adics" 0 THEN Auto) }
1
1. p : ℕ+
2. n : ℕ+
⊢ (0(p) n) = 0 ∈ ℤ
2
1. p : ℕ+
2. n : ℕ+
⊢ p-shift(p;0(p);n) = 0(p) ∈ (ℕ+ ⟶ ℤ)
Latex:
Latex:
No  Annotations
\mforall{}p,n:\mBbbN{}\msupplus{}.    (p-shift(p;0(p);n)  =  0(p))
By
Latex:
(Intros  THEN  RWO  "equal-p-adics"  0  THEN  Auto)
Home
Index