---

Step * of Lemma det-row-op

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[a,b:ℕn]. ∀[k:|r|].  |row-op(r;a;b;k;M)| = |M| ∈ |r| supposing ¬(a = b ∈ ℤ)
BY
{ (InstLemma `det-fun-row-op` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (D -1 With ⌜λM.|M|⌝  THENA (Auto THEN BLemma `matrix-det-is-det-fun` THEN Auto))
   THEN Reduce -1
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].  \mforall{}[a,b:\mBbbN{}n].  \mforall{}[k:|r|].
    |row-op(r;a;b;k;M)|  =  |M|  supposing  \mneg{}(a  =  b)


By

---

Latex:
(InstLemma  `det-fun-row-op`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  -1  With  \mkleeneopen{}\mlambda{}M.|M|\mkleeneclose{}    THENA  (Auto  THEN  BLemma  `matrix-det-is-det-fun`  THEN  Auto))
  THEN  Reduce  -1
  THEN  Trivial)

---

Home Index