Step
*
of Lemma
dot-product-comm
∀[n:ℕ]. ∀[x,y:ℝ^n].  (x ⋅ y = y ⋅ x)
BY
{ (RepUR ``real-vec dot-product`` 0
   THEN Auto
   THEN BLemma `rsum_functionality`
   THEN Auto
   THEN D 0
   THEN Auto
   THEN nRNorm 0
   THEN Auto) }
Latex:
Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    (x  \mcdot{}  y  =  y  \mcdot{}  x)
By
Latex:
(RepUR  ``real-vec  dot-product``  0
  THEN  Auto
  THEN  BLemma  `rsum\_functionality`
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  nRNorm  0
  THEN  Auto)
Home
Index