---

Step * of Lemma adjugate-transpose

∀[r:CRng]. ∀[n:ℕ]. ∀[M:Matrix(n;n;r)].  (adj(M') = adj(M)' ∈ Matrix(n;n;r))
BY
{ (Auto
   THEN RW (AddrC [3] (UnfoldC `matrix-transpose`)) 0
   THEN Unfold `adjugate` 0
   THEN EqCDA
   THEN Reduce 0
   THEN RWO "transpose-matrix-minor<" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RW  (AddrC  [3]  (UnfoldC  `matrix-transpose`))  0
  THEN  Unfold  `adjugate`  0
  THEN  EqCDA
  THEN  Reduce  0
  THEN  RWO  "transpose-matrix-minor<"  0
  THEN  Auto)

---

Home Index