---

Step * of Lemma matrix-minor_wf

∀[n,m:ℤ]. ∀[r:RngSig]. ∀[i:ℕn]. ∀[j:ℕm]. ∀[M:Matrix(n;m;r)].  (matrix-minor(i;j;M) ∈ Matrix(n - 1;m - 1;r))
BY
{ (Auto THEN Unfold `matrix` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[r:RngSig].  \mforall{}[i:\mBbbN{}n].  \mforall{}[j:\mBbbN{}m].  \mforall{}[M:Matrix(n;m;r)].
    (matrix-minor(i;j;M)  \mmember{}  Matrix(n  -  1;m  -  1;r))


By

---

Latex:
(Auto  THEN  Unfold  `matrix`  0  THEN  ProveWfLemma)

---

Home Index