---

Step * of Lemma determinant_wf

∀[r:CRng]. ∀[n:ℕ].  (determinant(n;r) ∈ Matrix(n;n;r) ⟶ |r|)
BY
{ (InductionOnNat
   THEN Unfold `determinant` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN (((Subst' (n =z 0) ~ ff 0 THENA Complete (Auto)) THEN Reduce 0 THEN Fold `determinant` 0 THEN Auto)
   ORELSE Auto
   )) }

---

Latex:

---

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


By

---

Latex:
(InductionOnNat
  THEN  Unfold  `determinant`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (((Subst'  (n  =\msubz{}  0)  \msim{}  ff  0  THENA  Complete  (Auto))
                THEN  Reduce  0
                THEN  Fold  `determinant`  0
                THEN  Auto)
  ORELSE  Auto
  ))

---

Home Index