:: deftheorem Def1 defines Part_sgn MATRIX11:def 1 :
for n being Nat
for K being commutative Ring
for perm2 being Element of Permutations (n + 2)
for b₄ being Function of (2Set (Seg (n + 2))), the carrier of K holds
( b₄ = Part_sgn (perm2,K) iff for i, j being Nat st i in Seg (n + 2) & j in Seg (n + 2) & i < j holds
( ( perm2 . i < perm2 . j implies b₄ . {i,j} = 1_ K ) & ( perm2 . i > perm2 . j implies b₄ . {i,j} = - (1_ K) ) ) );