---

Step * of Lemma swap-rows-is-transpose-swap-cols

∀[M,i,j:Top].  (matrix-swap-rows(M;i;j) ~ matrix-swap-cols(M';i;j)')
BY
{ (Auto THEN RepUR ``matrix-swap-rows matrix-swap-cols matrix-transpose`` 0 THEN RepUR ``mx matrix-ap`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[M,i,j:Top].    (matrix-swap-rows(M;i;j)  \msim{}  matrix-swap-cols(M';i;j)')


By

---

Latex:
(Auto
  THEN  RepUR  ``matrix-swap-rows  matrix-swap-cols  matrix-transpose``  0
  THEN  RepUR  ``mx  matrix-ap``  0
  THEN  Auto)

---

Home Index