Permutation group

-- set of permutations of k elements
def S k := {π  : {1, ..., k} : one-to-one π}

-- easy to compute cardinality:

lemma : |S k| = k! := sorry

• Important group;

  • Every finite group is subgroup of permutation group.

  • The Clifford group is a finite group.

-- cycle notation

-- example for k = 5

notation π = (1 3 5) (2 4) means

example : π(1) = 3 := refl

example : π(3) = 5 := refl

example : π(5) = 1 := refl

example : π(2) = 4 := refl

-- simple lemma

lemma : ⟨(1 2 ... k), (1 2)⟩ = S k := 
begin
  -- first step : 2-cycles generate S k, i.e., ⟨ {(i j)}_i < j ⟩ = S k

  -- Note: Inverse of a cycle is always a power of a cycle.
end