---

Step * 2 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. |A| | 1 in r
⊢ invertible-matrix(r;n;A)
BY
{ (D -1 THEN D 0 With ⌜c*adj(A)⌝  THEN Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -1  THEN  D  0  With  \mkleeneopen{}c*adj(A)\mkleeneclose{}    THEN  Auto)

---

Home Index