Permutations from a list

A list l : List α can be interpreted as an Equiv.Perm α where each element in the list is permuted to the next one, defined as formPerm. When we have that Nodup l, we prove that Equiv.Perm.support (formPerm l) = l.toFinset, and that formPerm l is rotationally invariant, in formPerm_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.formPerm 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.formPerm 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.formPerm to produce a nontrivial permutation that is noncyclic.

def List.formPerm {α : Type u_1} [DecidableEq α] (l : List α) : Equiv.Perm α

A list l : List α can be interpreted as an Equiv.Perm α where each element in the list is permuted to the next one, defined as formPerm. When we have that Nodup l, we prove that Equiv.Perm.support (formPerm l) = l.toFinset, and that formPerm l is rotationally invariant, in formPerm_rotate.

Equations

• List.formPerm l = List.prod (List.zipWith Equiv.swap l (List.tail l))

@[simp]

theorem List.formPerm_nil {α : Type u_1} [DecidableEq α] : List.formPerm [] = 1

@[simp]

theorem List.formPerm_singleton {α : Type u_1} [DecidableEq α] (x : α) : List.formPerm [x] = 1

@[simp]

theorem List.formPerm_cons_cons {α : Type u_1} [DecidableEq α] (x : α) (y : α) (l : List α) : List.formPerm (x :: y :: l) = Equiv.swap x y * List.formPerm (y :: l)

theorem List.formPerm_pair {α : Type u_1} [DecidableEq α] (x : α) (y : α) : List.formPerm [x, y] = Equiv.swap x y

theorem List.formPerm_apply_of_not_mem {α : Type u_1} [DecidableEq α] (x : α) (l : List α) (h : ¬x ∈ l) : ↑(List.formPerm l) x = x

theorem List.mem_of_formPerm_apply_ne {α : Type u_1} [DecidableEq α] (x : α) (l : List α) : ↑(List.formPerm l) x ≠ x → x ∈ l

theorem List.formPerm_apply_mem_of_mem {α : Type u_1} [DecidableEq α] (x : α) (l : List α) (h : x ∈ l) : ↑(List.formPerm l) x ∈ l

theorem List.mem_of_formPerm_apply_mem {α : Type u_1} [DecidableEq α] (x : α) (l : List α) (h : ↑(List.formPerm l) x ∈ l) : x ∈ l

theorem List.formPerm_mem_iff_mem {α : Type u_1} [DecidableEq α] {l : List α} {x : α} : ↑(List.formPerm l) x ∈ l ↔ x ∈ l

@[simp]

theorem List.formPerm_cons_concat_apply_last {α : Type u_1} [DecidableEq α] (x : α) (y : α) (xs : List α) : ↑(List.formPerm (x :: (xs ++ [y]))) y = x

@[simp]

theorem List.formPerm_apply_getLast {α : Type u_1} [DecidableEq α] (x : α) (xs : List α) : ↑(List.formPerm (x :: xs)) (List.getLast (x :: xs) (_ : x :: xs ≠ [])) = x

@[simp]

theorem List.formPerm_apply_nthLe_length {α : Type u_1} [DecidableEq α] (x : α) (xs : List α) : ↑(List.formPerm (x :: xs)) (List.nthLe (x :: xs) (List.length xs) (_ : List.length xs < Nat.succ (List.length xs))) = x

theorem List.formPerm_apply_head {α : Type u_1} [DecidableEq α] (x : α) (y : α) (xs : List α) (h : List.Nodup (x :: y :: xs)) : ↑(List.formPerm (x :: y :: xs)) x = y

theorem List.formPerm_apply_nthLe_zero {α : Type u_1} [DecidableEq α] (l : List α) (h : List.Nodup l) (hl : 1 < List.length l) : ↑(List.formPerm l) (List.nthLe l 0 (_ : 0 < List.length l)) = List.nthLe l 1 hl

theorem List.formPerm_eq_head_iff_eq_getLast {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (y : α) : ↑(List.formPerm (y :: l)) x = y ↔ x = List.getLast (y :: l) (_ : y :: l ≠ [])

theorem List.zipWith_swap_prod_support' {α : Type u_1} [DecidableEq α] (l : List α) (l' : List α) : {x | ↑(List.prod (List.zipWith Equiv.swap l l')) x ≠ x} ≤ ↑(List.toFinset l ⊔ List.toFinset l')

theorem List.zipWith_swap_prod_support {α : Type u_1} [DecidableEq α] [Fintype α] (l : List α) (l' : List α) : Equiv.Perm.support (List.prod (List.zipWith Equiv.swap l l')) ≤ List.toFinset l ⊔ List.toFinset l'

theorem List.support_formPerm_le' {α : Type u_1} [DecidableEq α] (l : List α) : {x | ↑(List.formPerm l) x ≠ x} ≤ ↑(List.toFinset l)

theorem List.support_formPerm_le {α : Type u_1} [DecidableEq α] (l : List α) [Fintype α] : Equiv.Perm.support (List.formPerm l) ≤ List.toFinset l

theorem List.formPerm_apply_lt {α : Type u_1} [DecidableEq α] (xs : List α) (h : List.Nodup xs) (n : ℕ) (hn : n + 1 < List.length xs) : ↑(List.formPerm xs) (List.nthLe xs n (_ : n < List.length xs)) = List.nthLe xs (n + 1) hn

theorem List.formPerm_apply_nthLe {α : Type u_1} [DecidableEq α] (xs : List α) (h : List.Nodup xs) (n : ℕ) (hn : n < List.length xs) : ↑(List.formPerm xs) (List.nthLe xs n hn) = List.nthLe xs ((n + 1) % List.length xs) (_ : (n + 1) % List.length xs < List.length xs)

theorem List.support_formPerm_of_nodup' {α : Type u_1} [DecidableEq α] (l : List α) (h : List.Nodup l) (h' : ∀ (x : α), l ≠ [x]) : {x | ↑(List.formPerm l) x ≠ x} = ↑(List.toFinset l)

theorem List.support_formPerm_of_nodup {α : Type u_1} [DecidableEq α] [Fintype α] (l : List α) (h : List.Nodup l) (h' : ∀ (x : α), l ≠ [x]) : Equiv.Perm.support (List.formPerm l) = List.toFinset l

theorem List.formPerm_rotate_one {α : Type u_1} [DecidableEq α] (l : List α) (h : List.Nodup l) : List.formPerm (List.rotate l 1) = List.formPerm l

theorem List.formPerm_rotate {α : Type u_1} [DecidableEq α] (l : List α) (h : List.Nodup l) (n : ℕ) : List.formPerm (List.rotate l n) = List.formPerm l

theorem List.formPerm_eq_of_isRotated {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} (hd : List.Nodup l) (h : l ~r l') : List.formPerm l = List.formPerm l'

theorem List.formPerm_reverse {α : Type u_1} [DecidableEq α] (l : List α) (h : List.Nodup l) : List.formPerm (List.reverse l) = (List.formPerm l)⁻¹

theorem List.formPerm_pow_apply_nthLe {α : Type u_1} [DecidableEq α] (l : List α) (h : List.Nodup l) (n : ℕ) (k : ℕ) (hk : k < List.length l) : ↑(List.formPerm l ^ n) (List.nthLe l k hk) = List.nthLe l ((k + n) % List.length l) (_ : (k + n) % List.length l < List.length l)

theorem List.formPerm_pow_apply_head {α : Type u_1} [DecidableEq α] (x : α) (l : List α) (h : List.Nodup (x :: l)) (n : ℕ) : ↑(List.formPerm (x :: l) ^ n) x = List.nthLe (x :: l) (n % List.length (x :: l)) (_ : n % List.length (x :: l) < List.length (x :: l))

theorem List.formPerm_ext_iff {α : Type u_1} [DecidableEq α] {x : α} {y : α} {x' : α} {y' : α} {l : List α} {l' : List α} (hd : List.Nodup (x :: y :: l)) (hd' : List.Nodup (x' :: y' :: l')) : List.formPerm (x :: y :: l) = List.formPerm (x' :: y' :: l') ↔ (x :: y :: l) ~r (x' :: y' :: l')

theorem List.formPerm_apply_mem_eq_self_iff {α : Type u_1} [DecidableEq α] (l : List α) (hl : List.Nodup l) (x : α) (hx : x ∈ l) : ↑(List.formPerm l) x = x ↔ List.length l ≤ 1

theorem List.formPerm_apply_mem_ne_self_iff {α : Type u_1} [DecidableEq α] (l : List α) (hl : List.Nodup l) (x : α) (hx : x ∈ l) : ↑(List.formPerm l) x ≠ x ↔ 2 ≤ List.length l

theorem List.mem_of_formPerm_ne_self {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (h : ↑(List.formPerm l) x ≠ x) : x ∈ l

theorem List.formPerm_eq_self_of_not_mem {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (h : ¬x ∈ l) : ↑(List.formPerm l) x = x

theorem List.formPerm_eq_one_iff {α : Type u_1} [DecidableEq α] (l : List α) (hl : List.Nodup l) : List.formPerm l = 1 ↔ List.length l ≤ 1

theorem List.formPerm_eq_formPerm_iff {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} (hl : List.Nodup l) (hl' : List.Nodup l') : List.formPerm l = List.formPerm l' ↔ l ~r l' ∨ List.length l ≤ 1 ∧ List.length l' ≤ 1

theorem List.form_perm_zpow_apply_mem_imp_mem {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (hx : x ∈ l) (n : ℤ) : ↑(List.formPerm l ^ n) x ∈ l

theorem List.formPerm_pow_length_eq_one_of_nodup {α : Type u_1} [DecidableEq α] (l : List α) (hl : List.Nodup l) : List.formPerm l ^ List.length l = 1