Step
*
of Lemma
pa-mul_wf
∀[p:{2...}]. ∀[x,y:basic-padic(p)]. (pa-mul(p;x;y) ∈ padic(p))
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[p:\{2...\}]. \mforall{}[x,y:basic-padic(p)]. (pa-mul(p;x;y) \mmember{} padic(p))
By
Latex:
ProveWfLemma
Home
Index