---

Step * 1 1 of Lemma matrix-det-is-determinant

.....assertion..... 
1. r : CRng
2. n : ℕ
3. (λm.|m|) = (λM.(((λm.|m|) I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|)
4. M : Matrix(n;n;r)
5. |M| = (|I| * (determinant(n;r) M)) ∈ |r|
⊢ (|I| * (determinant(n;r) M)) = (determinant(n;r) M) ∈ |r|
BY
{ (RWO "det-id" 0 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  (\mlambda{}m.|m|)  =  (\mlambda{}M.(((\mlambda{}m.|m|)  I)  *  (determinant(n;r)  M)))
4.  M  :  Matrix(n;n;r)
5.  |M|  =  (|I|  *  (determinant(n;r)  M))
\mvdash{}  (|I|  *  (determinant(n;r)  M))  =  (determinant(n;r)  M)


By

---

Latex:
(RWO  "det-id"  0  THEN  Auto)

---

Home Index