---

Step * of Lemma matrix-det-is-determinant

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].  (|M| = (determinant(n;r) M) ∈ |r|)
BY
{ (InstLemma `det-fun-is-determinant` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (D -1 With ⌜λm.|m|⌝  THENA (Auto THEN BLemma `matrix-det-is-det-fun` THEN Auto))) }

1
1. [r] : CRng
2. [n] : ℕ
3. (λm.|m|) = (λM.(((λm.|m|) I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|)
⊢ ∀[M:Matrix(n;n;r)]. (|M| = (determinant(n;r) M) ∈ |r|)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].    (|M|  =  (determinant(n;r)  M))


By

---

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

---

Home Index