---

Step * 1 1 of Lemma invertible-matrix-iff-det


1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. (A*adj(A)) = |A|*I ∈ Matrix(n;n;r)
5. B : Matrix(n;n;r)
6. (A*B) = I ∈ Matrix(n;n;r)
⊢ |A| | 1 in r
BY
{ ((Assert |(A*B)| = |I| ∈ |r| BY Auto) THEN (RWO "det-times det-id" (-1) THENA Auto)) }

1
1. r : CRng
2. n : ℕ
3. A : Matrix(n;n;r)
4. (A*adj(A)) = |A|*I ∈ Matrix(n;n;r)
5. B : Matrix(n;n;r)
6. (A*B) = I ∈ Matrix(n;n;r)
7. (|A| * |B|) = 1 ∈ |r|
⊢ |A| | 1 in r

---

Latex:

---

Latex:

1.  r  :  CRng
2.  n  :  \mBbbN{}
3.  A  :  Matrix(n;n;r)
4.  (A*adj(A))  =  |A|*I
5.  B  :  Matrix(n;n;r)
6.  (A*B)  =  I
\mvdash{}  |A|  |  1  in  r


By

---

Latex:
((Assert  |(A*B)|  =  |I|  BY  Auto)  THEN  (RWO  "det-times  det-id"  (-1)  THENA  Auto))

---

Home Index