Nuprl Definition : permutation-sign
The sign of a permutation can be defined in various ways.
The crucial properties are
1) Error :permutation-sign-id (sign of identity = 1)
2) Error :sign-flip (sign of a transposition = -1)
3) Error :permutation-sign-compose (sign of f o g = sign(f)*sign(g))
Properties 1 and 3 make sign a character of the group of permutations on
ℕn (the symmetric group Sn).
The definition used here suffices to prove these properties,
so it is equivalent to any other definition -- e.g parity of the number
of transpositons in a decompositon, etc.⋅
permutation-sign(n;f) == Π(Π(sign((f j) - f i) | i < j) | j < n)
Definitions occuring in Statement :
sign: sign(x),
int-prod: Π(f[x] | x < k),
apply: f a,
subtract: n - m
Definitions occuring in definition :
int-prod: Π(f[x] | x < k),
sign: sign(x),
subtract: n - m,
apply: f a
FDL editor aliases :
permutation-sign
Latex:
permutation-sign(n;f) == \mPi{}(\mPi{}(sign((f j) - f i) | i < j) | j < n)
Date html generated:
2018_05_21-PM-00_57_45
Last ObjectModification:
2017_12_11-AM-00_06_01
Theory : num_thy_1
Home
Index