Step
*
2
of Lemma
equal-padics
1. p : ℤ
2. x : padic(p)
3. y : padic(p)
4. x = y ∈ basic-padic(p)
⊢ x = y ∈ padic(p)
BY
{ ((D 2 THEN D -2) THEN Unfold `basic-padic` -1 THEN (EqHD (-1)⋅ THENA Auto) THEN All Reduce⋅) }
1
1. p : ℤ
2. n : ℕ
3. x1 : if (n =z 0) then p-adics(p) else p-units(p) fi
4. n1 : ℕ
5. y1 : if (n1 =z 0) then p-adics(p) else p-units(p) fi
6. n = n1 ∈ ℕ
7. x1 = y1 ∈ p-adics(p)
⊢ <n, x1> = <n1, y1> ∈ padic(p)
Latex:
Latex:
1. p : \mBbbZ{}
2. x : padic(p)
3. y : padic(p)
4. x = y
\mvdash{} x = y
By
Latex:
((D 2 THEN D -2) THEN Unfold `basic-padic` -1 THEN (EqHD (-1)\mcdot{} THENA Auto) THEN All Reduce\mcdot{})
Home
Index