---

Step * of Lemma real-det-sq-matrix-det

∀n:ℕ. ∀M:Top.  (|M| ~ |M|)
BY
{ (Auto THEN RepUR ``real-det matrix-det rng_lsum rng_prod mon_itop matrix-ap`` 0 THEN Fold `r-list-sum` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}M:Top.    (|M|  \msim{}  |M|)


By

---

Latex:
(Auto
  THEN  RepUR  ``real-det  matrix-det  rng\_lsum  rng\_prod  mon\_itop  matrix-ap``  0
  THEN  Fold  `r-list-sum`  0
  THEN  Auto)

---

Home Index