---

Step * of Lemma det-mul-col

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)]. ∀[i:ℕn]. ∀[k:|r|].  (|matrix-mul-col(r;k;i;M)| = (k * |M|) ∈ |r|)
BY
{ (Auto THEN RWW "mul-col-is-transpose-mul-row det-transpose det-mul-row" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].  \mforall{}[i:\mBbbN{}n].  \mforall{}[k:|r|].    (|matrix-mul-col(r;k;i;M)|  =  (k  *  |M|))


By

---

Latex:
(Auto  THEN  RWW  "mul-col-is-transpose-mul-row  det-transpose  det-mul-row"  0  THEN  Auto)

---

Home Index