mathlib3 documentation

group_theory.perm.list

Permutations from a list #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A list l : list α can be interpreted as a equiv.perm α where each element in the list is permuted to the next one, defined as form_perm. When we have that nodup l, we prove that equiv.perm.support (form_perm l) = l.to_finset, and that form_perm l is rotationally invariant, in form_perm_rotate.

When there are duplicate elements in l, how and in what arrangement with respect to the other elements they appear in the list determines the formed permutation. This is because list.form_perm is implemented as a product of equiv.swaps. That means that presence of a sublist of two adjacent duplicates like [..., x, x, ...] will produce the same permutation as if the adjacent duplicates were not present.

The list.form_perm definition is meant to primarily be used with nodup l, so that the resulting permutation is cyclic (if l has at least two elements). The presence of duplicates in a particular placement can lead list.form_perm to produce a nontrivial permutation that is noncyclic.

def list.form_perm {α : Type u_1} [decidable_eq α] (l : list α) :

A list l : list α can be interpreted as a equiv.perm α where each element in the list is permuted to the next one, defined as form_perm. When we have that nodup l, we prove that equiv.perm.support (form_perm l) = l.to_finset, and that form_perm l is rotationally invariant, in form_perm_rotate.

Equations
@[simp]
theorem list.form_perm_nil {α : Type u_1} [decidable_eq α] :
@[simp]
theorem list.form_perm_singleton {α : Type u_1} [decidable_eq α] (x : α) :
@[simp]
theorem list.form_perm_cons_cons {α : Type u_1} [decidable_eq α] (x y : α) (l : list α) :
(x :: y :: l).form_perm = equiv.swap x y * (y :: l).form_perm
theorem list.form_perm_pair {α : Type u_1} [decidable_eq α] (x y : α) :
theorem list.form_perm_apply_of_not_mem {α : Type u_1} [decidable_eq α] (x : α) (l : list α) (h : x l) :
(l.form_perm) x = x
theorem list.mem_of_form_perm_apply_ne {α : Type u_1} [decidable_eq α] (x : α) (l : list α) :
(l.form_perm) x x x l
theorem list.form_perm_apply_mem_of_mem {α : Type u_1} [decidable_eq α] (x : α) (l : list α) (h : x l) :
theorem list.mem_of_form_perm_apply_mem {α : Type u_1} [decidable_eq α] (x : α) (l : list α) (h : (l.form_perm) x l) :
x l
theorem list.form_perm_mem_iff_mem {α : Type u_1} [decidable_eq α] {l : list α} {x : α} :
(l.form_perm) x l x l
@[simp]
theorem list.form_perm_cons_concat_apply_last {α : Type u_1} [decidable_eq α] (x y : α) (xs : list α) :
((x :: (xs ++ [y])).form_perm) y = x
@[simp]
theorem list.form_perm_apply_last {α : Type u_1} [decidable_eq α] (x : α) (xs : list α) :
((x :: xs).form_perm) ((x :: xs).last _) = x
@[simp]
theorem list.form_perm_apply_nth_le_length {α : Type u_1} [decidable_eq α] (x : α) (xs : list α) :
((x :: xs).form_perm) ((x :: xs).nth_le xs.length _) = x
theorem list.form_perm_apply_head {α : Type u_1} [decidable_eq α] (x y : α) (xs : list α) (h : (x :: y :: xs).nodup) :
((x :: y :: xs).form_perm) x = y
theorem list.form_perm_apply_nth_le_zero {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (hl : 1 < l.length) :
(l.form_perm) (l.nth_le 0 _) = l.nth_le 1 hl
theorem list.form_perm_eq_head_iff_eq_last {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) :
((y :: l).form_perm) x = y x = (y :: l).last _
theorem list.zip_with_swap_prod_support' {α : Type u_1} [decidable_eq α] (l l' : list α) :
theorem list.support_form_perm_le' {α : Type u_1} [decidable_eq α] (l : list α) :
{x : α | (l.form_perm) x x} (l.to_finset)
theorem list.form_perm_apply_lt {α : Type u_1} [decidable_eq α] (xs : list α) (h : xs.nodup) (n : ) (hn : n + 1 < xs.length) :
(xs.form_perm) (xs.nth_le n _) = xs.nth_le (n + 1) hn
theorem list.form_perm_apply_nth_le {α : Type u_1} [decidable_eq α] (xs : list α) (h : xs.nodup) (n : ) (hn : n < xs.length) :
(xs.form_perm) (xs.nth_le n hn) = xs.nth_le ((n + 1) % xs.length) _
theorem list.support_form_perm_of_nodup' {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (h' : (x : α), l [x]) :
{x : α | (l.form_perm) x x} = (l.to_finset)
theorem list.support_form_perm_of_nodup {α : Type u_1} [decidable_eq α] [fintype α] (l : list α) (h : l.nodup) (h' : (x : α), l [x]) :
theorem list.form_perm_rotate_one {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) :
theorem list.form_perm_rotate {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (n : ) :
theorem list.form_perm_eq_of_is_rotated {α : Type u_1} [decidable_eq α] {l l' : list α} (hd : l.nodup) (h : l ~r l') :
theorem list.form_perm_reverse {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) :
theorem list.form_perm_pow_apply_nth_le {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (n k : ) (hk : k < l.length) :
(l.form_perm ^ n) (l.nth_le k hk) = l.nth_le ((k + n) % l.length) _
theorem list.form_perm_pow_apply_head {α : Type u_1} [decidable_eq α] (x : α) (l : list α) (h : (x :: l).nodup) (n : ) :
((x :: l).form_perm ^ n) x = (x :: l).nth_le (n % (x :: l).length) _
theorem list.form_perm_ext_iff {α : Type u_1} [decidable_eq α] {x y x' y' : α} {l l' : list α} (hd : (x :: y :: l).nodup) (hd' : (x' :: y' :: l').nodup) :
(x :: y :: l).form_perm = (x' :: y' :: l').form_perm (x :: y :: l) ~r (x' :: y' :: l')
theorem list.form_perm_apply_mem_eq_self_iff {α : Type u_1} [decidable_eq α] (l : list α) (hl : l.nodup) (x : α) (hx : x l) :
theorem list.form_perm_apply_mem_ne_self_iff {α : Type u_1} [decidable_eq α] (l : list α) (hl : l.nodup) (x : α) (hx : x l) :
theorem list.mem_of_form_perm_ne_self {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : (l.form_perm) x x) :
x l
theorem list.form_perm_eq_self_of_not_mem {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : x l) :
(l.form_perm) x = x
theorem list.form_perm_eq_one_iff {α : Type u_1} [decidable_eq α] (l : list α) (hl : l.nodup) :
theorem list.form_perm_eq_form_perm_iff {α : Type u_1} [decidable_eq α] {l l' : list α} (hl : l.nodup) (hl' : l'.nodup) :
theorem list.form_perm_zpow_apply_mem_imp_mem {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (hx : x l) (n : ) :
(l.form_perm ^ n) x l
theorem list.form_perm_pow_length_eq_one_of_nodup {α : Type u_1} [decidable_eq α] (l : list α) (hl : l.nodup) :