let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum