---

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

.....basecase..... 
1. r : CRng
2. n : ℤ
⊢ ∀[d:det-fun(r;0)]. (d = (λM.((d I) * (determinant(0;r) M))) ∈ (Matrix(0;0;r) ⟶ |r|))
BY
{ (Auto
   THEN ((FunExt THENA Auto) THEN Reduce 0)
   THEN RepUR ``determinant`` 0
   THEN (D 3 THEN Auto)
   THEN (RW RngNormC 0 THENA Auto)
   THEN EqCDA
   THEN RepUR ``matrix`` 0
   THEN FunExt
   THEN Auto) }

---

Latex:

---

Latex:
.....basecase..... 
1.  r  :  CRng
2.  n  :  \mBbbZ{}
\mvdash{}  \mforall{}[d:det-fun(r;0)].  (d  =  (\mlambda{}M.((d  I)  *  (determinant(0;r)  M))))


By

---

Latex:
(Auto
  THEN  ((FunExt  THENA  Auto)  THEN  Reduce  0)
  THEN  RepUR  ``determinant``  0
  THEN  (D  3  THEN  Auto)
  THEN  (RW  RngNormC  0  THENA  Auto)
  THEN  EqCDA
  THEN  RepUR  ``matrix``  0
  THEN  FunExt
  THEN  Auto)

---

Home Index