---

Step * of Lemma mul-row-is-transpose-mul-col

∀[M,r,i,k:Top].  (matrix-mul-row(r;k;i;M) ~ matrix-mul-col(r;k;i;M')')
BY
{ (Auto THEN RepUR ``matrix-mul-row matrix-mul-col matrix-transpose`` 0 THEN RepUR ``mx matrix-ap`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[M,r,i,k:Top].    (matrix-mul-row(r;k;i;M)  \msim{}  matrix-mul-col(r;k;i;M')')


By

---

Latex:
(Auto
  THEN  RepUR  ``matrix-mul-row  matrix-mul-col  matrix-transpose``  0
  THEN  RepUR  ``mx  matrix-ap``  0
  THEN  Auto)

---

Home Index