---

Step * 1 of Lemma bpa-norm_wf_padic


1. p : ℕ+
2. n : ℕ
3. a : p-adics(p)
⊢ bpa-norm(p;<n, a>) ∈ padic(p)
BY
{ (Unfold `padic` 0 THEN (GenConclTerm ⌜bpa-norm(p;<n, a>)⌝⋅ THENA Auto) THEN D -2 THEN MemCD THEN Auto THEN AutoSplit) \000C}

1
1. p : ℕ+
2. n : ℕ
3. a : p-adics(p)
4. v1 : {1...}
5. v2 : p-adics(p)
6. bpa-norm(p;<n, a>) = <v1, v2> ∈ basic-padic(p)
⊢ v2 ∈ p-units(p)

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}\msupplus{}
2.  n  :  \mBbbN{}
3.  a  :  p-adics(p)
\mvdash{}  bpa-norm(p;<n,  a>)  \mmember{}  padic(p)


By

---

Latex:
(Unfold  `padic`  0
  THEN  (GenConclTerm  \mkleeneopen{}bpa-norm(p;<n,  a>)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  MemCD
  THEN  Auto
  THEN  AutoSplit)

---

Home Index