---

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

No Annotations
∀n:ℕ. ∀M:ℕn ⟶ ℕn ⟶ ℝ.  (|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 (BLemma `r-list-sum_functionality` THENW Auto)
   THEN RWO "map-length" 0
   THEN Auto
   THEN (RWO "select-map" 0 THENA Auto)
   THEN Reduce 0) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}M:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}.    (|M|  =  |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  (BLemma  `r-list-sum\_functionality`  THENW  Auto)
  THEN  RWO  "map-length"  0
  THEN  Auto
  THEN  (RWO  "select-map"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index