Step
*
of Lemma
matrix-det_wf
∀[r:Rng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].  (|M| ∈ |r|)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[r:Rng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].    (|M|  \mmember{}  |r|)
By
Latex:
ProveWfLemma
Home
Index