---

Step * of Lemma invertible-matrix-iff-left

∀r:CRng. ∀n:ℕ. ∀A:Matrix(n;n;r).  (invertible-matrix(r;n;A) ⇐⇒ ∃B:Matrix(n;n;r). ((B*A) = I ∈ Matrix(n;n;r)))
BY
{ (Intros
   THEN (RWO "invertible-matrix-iff-det" 0 THENA Auto)
   THEN InstLemma `adjugate-property2` [⌜r⌝;⌜n⌝;⌜A⌝]⋅
   THEN Auto) }

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

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

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}n:\mBbbN{}.  \mforall{}A:Matrix(n;n;r).    (invertible-matrix(r;n;A)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}B:Matrix(n;n;r).  ((B*A)  =  I))


By

---

Latex:
(Intros
  THEN  (RWO  "invertible-matrix-iff-det"  0  THENA  Auto)
  THEN  InstLemma  `adjugate-property2`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index