:: deftheorem defines - MATRIX_1:def 16 :
for K being Ring
for n being Nat
for x being Element of K
for p being Element of Permutations n holds
( ( p is even implies - (x,p) = x ) & ( not p is even implies - (x,p) = - x ) );