---

Step * of Lemma invertible-matrix-iff-det

∀r:CRng. ∀n:ℕ. ∀A:Matrix(n;n;r).  (invertible-matrix(r;n;A) ⇐⇒ |A| | 1 in r)
BY
{ (InstLemma `adjugate-property` [] THEN RepeatFor 3 (ParallelLast') 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. invertible-matrix(r;n;A)
⊢ |A| | 1 in r

2
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)

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}n:\mBbbN{}.  \mforall{}A:Matrix(n;n;r).    (invertible-matrix(r;n;A)  \mLeftarrow{}{}\mRightarrow{}  |A|  |  1  in  r)


By

---

Latex:
(InstLemma  `adjugate-property`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  Auto)

---

Home Index