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