let n be Nat; for K being Field
for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
Minor (M,i,j) = Minor ((M @),j,i)
let K be Field; for M being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n holds
Minor (M,i,j) = Minor ((M @),j,i)
let M be Matrix of n,K; for i, j being Nat st i in Seg n & j in Seg n holds
Minor (M,i,j) = Minor ((M @),j,i)
let i, j be Nat; ( i in Seg n & j in Seg n implies Minor (M,i,j) = Minor ((M @),j,i) )
assume that
A1:
i in Seg n
and
A2:
j in Seg n
; Minor (M,i,j) = Minor ((M @),j,i)
thus Minor (M,i,j) =
Det ((Delete (M,i,j)) @)
by MATRIXR2:43
.=
Minor ((M @),j,i)
by A1, A2, Th14
; verum