let n be Nat; for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds
for M being Matrix of n,K
for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm)
let K be commutative Ring; ( not K is degenerated & K is well-unital & K is domRing-like implies for M being Matrix of n,K
for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm) )
assume A0:
( not K is degenerated & K is well-unital & K is domRing-like )
; for M being Matrix of n,K
for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm)
let M be Matrix of n,K; for perm being Element of Permutations n
for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm)
let perm be Element of Permutations n; for Perm being Permutation of (Seg n) st perm = Perm holds
Det (M * Perm) = - ((Det M),perm)
let Perm be Permutation of (Seg n); ( perm = Perm implies Det (M * Perm) = - ((Det M),perm) )
assume A1:
Perm = perm
; Det (M * Perm) = - ((Det M),perm)