---

Step * 2 of Lemma det-times


1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. B : Matrix(n;n;r)
5. λA.|(A*B)| ∈ det-fun(r;n)
⊢ |(A*B)| = (|A| * |B|) ∈ |r|
BY
{ (InstLemma `det-fun-is-determinant` [⌜r⌝;⌜n⌝;⌜λA.|(A*B)|⌝]⋅ THENA Auto) }

1
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. B : Matrix(n;n;r)
5. λA.|(A*B)| ∈ det-fun(r;n)
6. (λA.|(A*B)|) = (λM.(((λA.|(A*B)|) I) * (determinant(n;r) M))) ∈ (Matrix(n;n;r) ⟶ |r|)
⊢ |(A*B)| = (|A| * |B|) ∈ |r|

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  A  :  Matrix(n;n;r)
4.  B  :  Matrix(n;n;r)
5.  \mlambda{}A.|(A*B)|  \mmember{}  det-fun(r;n)
\mvdash{}  |(A*B)|  =  (|A|  *  |B|)


By

---

Latex:
(InstLemma  `det-fun-is-determinant`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}A.|(A*B)|\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index