equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section \<open>Permutations, both general and specifically on finite sets.\<close> |
5 section \<open>Permutations, both general and specifically on finite sets.\<close> |
6 |
6 |
7 theory Permutations |
7 theory Permutations |
8 imports Binomial Multiset Disjoint_Sets |
8 imports Multiset Disjoint_Sets |
9 begin |
9 begin |
10 |
10 |
11 subsection \<open>Transpositions\<close> |
11 subsection \<open>Transpositions\<close> |
12 |
12 |
13 lemma swap_id_idempotent [simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id" |
13 lemma swap_id_idempotent [simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id" |