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