Step
*
of Lemma
qdot_wf
∀[as,bs:ℚ List].  qdot(as;bs) ∈ ℚ supposing dimension(as) = dimension(bs) ∈ ℤ
BY
{ (RepUR ``qdot qv-dim`` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[as,bs:\mBbbQ{}  List].    qdot(as;bs)  \mmember{}  \mBbbQ{}  supposing  dimension(as)  =  dimension(bs)
By
Latex:
(RepUR  ``qdot  qv-dim``  0  THEN  Auto)
Home
Index