---

Step * of Lemma det-fun-is-determinant

∀[r:CRng]. ∀[n:ℕ]. ∀[d:det-fun(r;n)].  (d = (λM.((d I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|))
BY
{ InductionOnNat }

1
.....basecase..... 
1. r : CRng
2. n : ℤ
⊢ ∀[d:det-fun(r;0)]. (d = (λM.((d I) * (determinant(0;r) M))) ∈ (Matrix(0;0;r) ⟶ |r|))

2
.....upcase..... 
1. r : CRng
2. n : ℤ
3. 0 < n
4. ∀[d:det-fun(r;n - 1)]. (d = (λM.((d I) * (determinant(n - 1;r) M))) ∈ (Matrix(n - 1;n - 1;r) ⟶ |r|))
⊢ ∀[d:det-fun(r;n)]. (d = (λM.((d I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|))

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[d:det-fun(r;n)].    (d  =  (\mlambda{}M.((d  I)  *  (determinant(n;r)  M))))


By

---

Latex:
InductionOnNat

---

Home Index