---

Step * 1 1 of Lemma mkpadic_functionality


1. p : {2...}
2. v : padic(p)
3. v1 : padic(p)
⊢ (v = v1 ∈ basic-padic(p)) ⇒ (v = v1 ∈ padic(p))
BY
{ ((D 0 THENA Auto) THEN Unfold `basic-padic` -1) }

1
1. p : {2...}
2. v : padic(p)
3. v1 : padic(p)
4. v = v1 ∈ (ℕ × p-adics(p))
⊢ v = v1 ∈ padic(p)

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  v  :  padic(p)
3.  v1  :  padic(p)
\mvdash{}  (v  =  v1)  {}\mRightarrow{}  (v  =  v1)


By

---

Latex:
((D  0  THENA  Auto)  THEN  Unfold  `basic-padic`  -1)

---

Home Index