---

Step * of Lemma det-swap-rows

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i,j:ℕn].  |matrix-swap-rows(M;i;j)| = (-r |M|) ∈ |r| supposing ¬(i = j ∈ ℤ)
BY
{ (Auto THEN (RWO "swap-rows-is-transpose-swap-cols" 0 THENA Auto) THEN RWW "det-transpose det-swap-cols" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].  \mforall{}[i,j:\mBbbN{}n].
    |matrix-swap-rows(M;i;j)|  =  (-r  |M|)  supposing  \mneg{}(i  =  j)


By

---

Latex:
(Auto
  THEN  (RWO  "swap-rows-is-transpose-swap-cols"  0  THENA  Auto)
  THEN  RWW  "det-transpose  det-swap-cols"  0
  THEN  Auto)

---

Home Index