Step
*
2
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. c : |r|
6. (c * |A|) = 1 ∈ |r|
⊢ c*(A*adj(A)) = I ∈ Matrix(n;n;r)
BY
{ (RWO  "-3" 0 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. c : |r|
6. (c * |A|) = 1 ∈ |r|
⊢ c*|A|*I = 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.  c  :  |r|
6.  (c  *  |A|)  =  1
\mvdash{}  c*(A*adj(A))  =  I
By
Latex:
(RWO    "-3"  0  THENA  Auto)
Home
Index