# Permutations of Fin n#

Permutations of Fin (n + 1) are equivalent to fixing a single Fin (n + 1) and permuting the remaining with a Perm (Fin n). The fixed Fin (n + 1) is swapped with 0.

Equations
Instances For
@[simp]
theorem Equiv.Perm.decomposeFin_symm_of_refl {n : } (p : Fin (n + 1)) :
Equiv.Perm.decomposeFin.symm (p, Equiv.refl (Fin n)) =
@[simp]
theorem Equiv.Perm.decomposeFin_symm_of_one {n : } (p : Fin (n + 1)) :
Equiv.Perm.decomposeFin.symm (p, 1) =
@[simp]
theorem Equiv.Perm.decomposeFin_symm_apply_zero {n : } (p : Fin (n + 1)) (e : Equiv.Perm (Fin n)) :
(Equiv.Perm.decomposeFin.symm (p, e)) 0 = p
@[simp]
theorem Equiv.Perm.decomposeFin_symm_apply_succ {n : } (e : Equiv.Perm (Fin n)) (p : Fin (n + 1)) (x : Fin n) :
(Equiv.Perm.decomposeFin.symm (p, e)) x.succ = (Equiv.swap 0 p) (e x).succ
@[simp]
theorem Equiv.Perm.decomposeFin_symm_apply_one {n : } (e : Equiv.Perm (Fin (n + 1))) (p : Fin (n + 2)) :
(Equiv.Perm.decomposeFin.symm (p, e)) 1 = (Equiv.swap 0 p) (e 0).succ
@[simp]
theorem Equiv.Perm.decomposeFin.symm_sign {n : } (p : Fin (n + 1)) (e : Equiv.Perm (Fin n)) :
Equiv.Perm.sign (Equiv.Perm.decomposeFin.symm (p, e)) = (if p = 0 then 1 else -1) * Equiv.Perm.sign e
theorem Finset.univ_perm_fin_succ {n : } :
Finset.univ = Finset.map Equiv.Perm.decomposeFin.symm.toEmbedding Finset.univ

The set of all permutations of Fin (n + 1) can be constructed by augmenting the set of permutations of Fin n by each element of Fin (n + 1) in turn.

### cycleRange section #

Define the permutations Fin.cycleRange i, the cycle (0 1 2 ... i).

theorem finRotate_succ_eq_decomposeFin {n : } :
finRotate n.succ = Equiv.Perm.decomposeFin.symm (1, )
@[simp]
theorem sign_finRotate (n : ) :
Equiv.Perm.sign (finRotate (n + 1)) = (-1) ^ n
@[simp]
theorem support_finRotate {n : } :
(finRotate (n + 2)).support = Finset.univ
theorem support_finRotate_of_le {n : } (h : 2 n) :
(finRotate n).support = Finset.univ
theorem isCycle_finRotate {n : } :
(finRotate (n + 2)).IsCycle
theorem isCycle_finRotate_of_le {n : } (h : 2 n) :
(finRotate n).IsCycle
@[simp]
theorem cycleType_finRotate {n : } :
(finRotate (n + 2)).cycleType = {n + 2}
theorem cycleType_finRotate_of_le {n : } (h : 2 n) :
(finRotate n).cycleType = {n}
def Fin.cycleRange {n : } (i : Fin n) :

Fin.cycleRange i is the cycle (0 1 2 ... i) leaving (i+1 ... (n-1)) unchanged.

Equations
Instances For
theorem Fin.cycleRange_of_gt {n : } {i : Fin n.succ} {j : Fin n.succ} (h : i < j) :
i.cycleRange j = j
theorem Fin.cycleRange_of_le {n : } {i : Fin n.succ} {j : Fin n.succ} (h : j i) :
i.cycleRange j = if j = i then 0 else j + 1
theorem Fin.coe_cycleRange_of_le {n : } {i : Fin n.succ} {j : Fin n.succ} (h : j i) :
(i.cycleRange j) = if j = i then 0 else j + 1
theorem Fin.cycleRange_of_lt {n : } {i : Fin n.succ} {j : Fin n.succ} (h : j < i) :
i.cycleRange j = j + 1
theorem Fin.coe_cycleRange_of_lt {n : } {i : Fin n.succ} {j : Fin n.succ} (h : j < i) :
(i.cycleRange j) = j + 1
theorem Fin.cycleRange_of_eq {n : } {i : Fin n.succ} {j : Fin n.succ} (h : j = i) :
i.cycleRange j = 0
@[simp]
theorem Fin.cycleRange_self {n : } (i : Fin n.succ) :
i.cycleRange i = 0
theorem Fin.cycleRange_apply {n : } (i : Fin n.succ) (j : Fin n.succ) :
i.cycleRange j = if j < i then j + 1 else if j = i then 0 else j
@[simp]
theorem Fin.cycleRange_zero (n : ) :
@[simp]
theorem Fin.cycleRange_last (n : ) :
(Fin.last n).cycleRange = finRotate (n + 1)
@[simp]
theorem Fin.cycleRange_zero' {n : } (h : 0 < n) :
0, h.cycleRange = 1
@[simp]
theorem Fin.sign_cycleRange {n : } (i : Fin n) :
Equiv.Perm.sign i.cycleRange = (-1) ^ i
@[simp]
theorem Fin.succAbove_cycleRange {n : } (i : Fin n) (j : Fin n) :
i.succ.succAbove (i.cycleRange j) = (Equiv.swap 0 i.succ) j.succ
@[simp]
theorem Fin.cycleRange_succAbove {n : } (i : Fin (n + 1)) (j : Fin n) :
i.cycleRange (i.succAbove j) = j.succ
@[simp]
theorem Fin.cycleRange_symm_zero {n : } (i : Fin (n + 1)) :
(Equiv.symm i.cycleRange) 0 = i
@[simp]
theorem Fin.cycleRange_symm_succ {n : } (i : Fin (n + 1)) (j : Fin n) :
(Equiv.symm i.cycleRange) j.succ = i.succAbove j
theorem Fin.isCycle_cycleRange {n : } {i : Fin (n + 1)} (h0 : i 0) :
i.cycleRange.IsCycle
@[simp]
theorem Fin.cycleType_cycleRange {n : } {i : Fin (n + 1)} (h0 : i 0) :
i.cycleRange.cycleType = {i + 1}
theorem Fin.isThreeCycle_cycleRange_two {n : } :
.IsThreeCycle