mathlib3 documentation

group_theory.perm.fin

Permutations of fin n #

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

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
@[simp]
theorem equiv.perm.decompose_fin_symm_apply_zero {n : } (p : fin (n + 1)) (e : equiv.perm (fin n)) :
@[simp]
theorem equiv.perm.decompose_fin_symm_apply_succ {n : } (e : equiv.perm (fin n)) (p : fin (n + 1)) (x : fin n) :
@[simp]
theorem equiv.perm.decompose_fin_symm_apply_one {n : } (e : equiv.perm (fin (n + 1))) (p : fin (n + 2)) :
@[simp]

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.

cycle_range section #

Define the permutations fin.cycle_range i, the cycle (0 1 2 ... i).

@[simp]
theorem sign_fin_rotate (n : ) :
@[simp]
theorem is_cycle_fin_rotate {n : } :
theorem is_cycle_fin_rotate_of_le {n : } (h : 2 n) :
@[simp]
theorem cycle_type_fin_rotate {n : } :
(fin_rotate (n + 2)).cycle_type = {n + 2}
theorem cycle_type_fin_rotate_of_le {n : } (h : 2 n) :
def fin.cycle_range {n : } (i : fin n) :

fin.cycle_range i is the cycle (0 1 2 ... i) leaving (i+1 ... (n-1)) unchanged.

Equations
theorem fin.cycle_range_of_gt {n : } {i j : fin n.succ} (h : i < j) :
theorem fin.cycle_range_of_le {n : } {i j : fin n.succ} (h : j i) :
(i.cycle_range) j = ite (j = i) 0 (j + 1)
theorem fin.coe_cycle_range_of_le {n : } {i j : fin n.succ} (h : j i) :
((i.cycle_range) j) = ite (j = i) 0 (j + 1)
theorem fin.cycle_range_of_lt {n : } {i j : fin n.succ} (h : j < i) :
(i.cycle_range) j = j + 1
theorem fin.coe_cycle_range_of_lt {n : } {i j : fin n.succ} (h : j < i) :
theorem fin.cycle_range_of_eq {n : } {i j : fin n.succ} (h : j = i) :
@[simp]
theorem fin.cycle_range_self {n : } (i : fin n.succ) :
theorem fin.cycle_range_apply {n : } (i j : fin n.succ) :
(i.cycle_range) j = ite (j < i) (j + 1) (ite (j = i) 0 j)
@[simp]
theorem fin.cycle_range_zero (n : ) :
@[simp]
@[simp]
theorem fin.cycle_range_zero' {n : } (h : 0 < n) :
0, h⟩.cycle_range = 1
@[simp]
theorem fin.sign_cycle_range {n : } (i : fin n) :
@[simp]
theorem fin.succ_above_cycle_range {n : } (i j : fin n) :
@[simp]
theorem fin.cycle_range_succ_above {n : } (i : fin (n + 1)) (j : fin n) :
@[simp]
theorem fin.cycle_range_symm_zero {n : } (i : fin (n + 1)) :
@[simp]
theorem fin.cycle_range_symm_succ {n : } (i : fin (n + 1)) (j : fin n) :
theorem fin.is_cycle_cycle_range {n : } {i : fin (n + 1)} (h0 : i 0) :
@[simp]
theorem fin.cycle_type_cycle_range {n : } {i : fin (n + 1)} (h0 : i 0) :