Step
*
of Lemma
p-digits_wf
∀[p:ℕ+]. ∀[a:p-adics(p)].  (p-digits(p;a) ∈ ℕ+ ⟶ ℕp)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[p:\mBbbN{}\msupplus{}].  \mforall{}[a:p-adics(p)].    (p-digits(p;a)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}p)
By
Latex:
ProveWfLemma
Home
Index