---

Step * of Lemma diagonal-matrix_wf

∀[r:RngSig]. ∀[n:ℕ]. ∀[F:ℕn ⟶ |r|].  (diagonal-matrix(r;i.F[i]) ∈ Matrix(n;n;r))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[r:RngSig].  \mforall{}[n:\mBbbN{}].  \mforall{}[F:\mBbbN{}n  {}\mrightarrow{}  |r|].    (diagonal-matrix(r;i.F[i])  \mmember{}  Matrix(n;n;r))


By

---

Latex:
ProveWfLemma

---

Home Index