---

Step * of Lemma adjugate-property2

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].  ((adj(M)*M) = |M|*I ∈ Matrix(n;n;r))
BY
{ (Auto
   THEN EqualTranspose
   THEN (RWW "matrix-transpose-times transpose-scalar-mul adjugate-transpose<" 0 THENA Auto)
   THEN (RWW "adjugate-property det-transpose" 0 THENA Auto)) }

1
1. r : CRng
2. n : ℕ
3. M : Matrix(n;n;r)
⊢ |M|*I = |M|*I' ∈ Matrix(n;n;r)

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[M:Matrix(n;n;r)].    ((adj(M)*M)  =  |M|*I)


By

---

Latex:
(Auto
  THEN  EqualTranspose
  THEN  (RWW  "matrix-transpose-times  transpose-scalar-mul  adjugate-transpose<"  0  THENA  Auto)
  THEN  (RWW  "adjugate-property  det-transpose"  0  THENA  Auto))

---

Home Index