mathlib docs: group_theory.perm.sign

source

def equiv.perm.subtype_perm {α : Type u} (f : equiv.perm α) {p : α → Prop} (h : ∀ (x : α), p x ↔ p (⇑f x)) :

equiv.perm {x // p x}

Equations

f.subtype_perm h = {to_fun := λ (x : {x // p x}), ⟨⇑f ↑x, _⟩, inv_fun := λ (x : {x // p x}), ⟨⇑f⁻¹ ↑x, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.perm.subtype_perm_one {α : Type u} (p : α → Prop) (h : ∀ (x : α), p x ↔ p (⇑1 x)) :

1.subtype_perm h = 1

source

def equiv.perm.of_subtype {α : Type u} {p : α → Prop} [decidable_pred p] :

equiv.perm (subtype p) →* equiv.perm α

Equations

equiv.perm.of_subtype = {to_fun := λ (f : equiv.perm (subtype p)), {to_fun := λ (x : α), dite (p x) (λ (h : p x), ↑(⇑f ⟨x, h⟩)) (λ (h : ¬p x), x), inv_fun := λ (x : α), dite (p x) (λ (h : p x), ↑(⇑f⁻¹ ⟨x, h⟩)) (λ (h : ¬p x), x), left_inv := _, right_inv := _}, map_one' := _, map_mul' := _}

source

theorem equiv.perm.eq_inv_iff_eq {α : Type u} {f : equiv.perm α} {x y : α} :

x = ⇑f⁻¹ y ↔ ⇑f x = y

source

theorem equiv.perm.inv_eq_iff_eq {α : Type u} {f : equiv.perm α} {x y : α} :

⇑f⁻¹ x = y ↔ x = ⇑f y

source

def equiv.perm.disjoint {α : Type u} (f g : equiv.perm α) :

Prop

Two permutations f and g are disjoint if their supports are disjoint, i.e., every element is fixed either by f, or by g.

Equations

f.disjoint g = ∀ (x : α), ⇑f x = x ∨ ⇑g x = x

source

theorem equiv.perm.disjoint.symm {α : Type u} {f g : equiv.perm α} (a : f.disjoint g) :

g.disjoint f

source

theorem equiv.perm.disjoint_comm {α : Type u} {f g : equiv.perm α} :

f.disjoint g ↔ g.disjoint f

source

theorem equiv.perm.disjoint_mul_comm {α : Type u} {f g : equiv.perm α} (h : f.disjoint g) :

f * g = g * f

source

@[simp]

theorem equiv.perm.disjoint_one_left {α : Type u} (f : equiv.perm α) :

1.disjoint f

source

@[simp]

theorem equiv.perm.disjoint_one_right {α : Type u} (f : equiv.perm α) :

f.disjoint 1

source

theorem equiv.perm.disjoint_mul_left {α : Type u} {f g h : equiv.perm α} (H1 : f.disjoint h) (H2 : g.disjoint h) :

(f * g).disjoint h

source

theorem equiv.perm.disjoint_mul_right {α : Type u} {f g h : equiv.perm α} (H1 : f.disjoint g) (H2 : f.disjoint h) :

f.disjoint (g * h)

source

theorem equiv.perm.disjoint_prod_right {α : Type u} {f : equiv.perm α} (l : list (equiv.perm α)) (h : ∀ (g : equiv.perm α), g ∈ l → f.disjoint g) :

f.disjoint l.prod

source

theorem equiv.perm.disjoint_prod_perm {α : Type u} {l₁ l₂ : list (equiv.perm α)} (hl : list.pairwise equiv.perm.disjoint l₁) (hp : l₁ ~ l₂) :

l₁.prod = l₂.prod

source

theorem equiv.perm.of_subtype_subtype_perm {α : Type u} {f : equiv.perm α} {p : α → Prop} [decidable_pred p] (h₁ : ∀ (x : α), p x ↔ p (⇑f x)) (h₂ : ∀ (x : α), ⇑f x ≠ x → p x) :

⇑equiv.perm.of_subtype (f.subtype_perm h₁) = f

source

theorem equiv.perm.of_subtype_apply_of_not_mem {α : Type u} {p : α → Prop} [decidable_pred p] (f : equiv.perm (subtype p)) {x : α} (hx : ¬p x) :

⇑(⇑equiv.perm.of_subtype f) x = x

source

theorem equiv.perm.mem_iff_of_subtype_apply_mem {α : Type u} {p : α → Prop} [decidable_pred p] (f : equiv.perm (subtype p)) (x : α) :

p x ↔ p (⇑(⇑equiv.perm.of_subtype f) x)

source

@[simp]

theorem equiv.perm.subtype_perm_of_subtype {α : Type u} {p : α → Prop} [decidable_pred p] (f : equiv.perm (subtype p)) :

(⇑equiv.perm.of_subtype f).subtype_perm _ = f

source

theorem equiv.perm.pow_apply_eq_self_of_apply_eq_self {α : Type u} {f : equiv.perm α} {x : α} (hfx : ⇑f x = x) (n : ℕ) :

⇑(f ^ n) x = x

source

theorem equiv.perm.gpow_apply_eq_self_of_apply_eq_self {α : Type u} {f : equiv.perm α} {x : α} (hfx : ⇑f x = x) (n : ℤ) :

⇑(f ^ n) x = x

source

theorem equiv.perm.pow_apply_eq_of_apply_apply_eq_self {α : Type u} {f : equiv.perm α} {x : α} (hffx : ⇑f (⇑f x) = x) (n : ℕ) :

⇑(f ^ n) x = x ∨ ⇑(f ^ n) x = ⇑f x

source

theorem equiv.perm.gpow_apply_eq_of_apply_apply_eq_self {α : Type u} {f : equiv.perm α} {x : α} (hffx : ⇑f (⇑f x) = x) (i : ℤ) :

⇑(f ^ i) x = x ∨ ⇑(f ^ i) x = ⇑f x

source

def equiv.perm.support {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) :

finset α

Equations

f.support = finset.filter (λ (x : α), ⇑f x ≠ x) finset.univ

source

@[simp]

theorem equiv.perm.mem_support {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :

x ∈ f.support ↔ ⇑f x ≠ x

source

def equiv.perm.is_swap {α : Type u} [decidable_eq α] (f : equiv.perm α) :

Prop

Equations

f.is_swap = ∃ (x y : α), x ≠ y ∧ f = equiv.swap x y

source

theorem equiv.perm.swap_mul_eq_mul_swap {α : Type u} [decidable_eq α] (f : equiv.perm α) (x y : α) :

(equiv.swap x y) * f = f * equiv.swap (⇑f⁻¹ x) (⇑f⁻¹ y)

source

theorem equiv.perm.mul_swap_eq_swap_mul {α : Type u} [decidable_eq α] (f : equiv.perm α) (x y : α) :

f * equiv.swap x y = (equiv.swap (⇑f x) (⇑f y)) * f

source

@[simp]

theorem equiv.perm.swap_mul_self_mul {α : Type u} [decidable_eq α] (i j : α) (σ : equiv.perm α) :

(equiv.swap i j) * (equiv.swap i j) * σ = σ

Multiplying a permutation with swap i j twice gives the original permutation.

This specialization of swap_mul_self is useful when using cosets of permutations.

source

theorem equiv.perm.swap_mul_eq_iff {α : Type u} [decidable_eq α] {i j : α} {σ : equiv.perm α} :

(equiv.swap i j) * σ = σ ↔ i = j

source

theorem equiv.perm.is_swap_of_subtype {α : Type u} [decidable_eq α] {p : α → Prop} [decidable_pred p] {f : equiv.perm (subtype p)} (h : f.is_swap) :

(⇑equiv.perm.of_subtype f).is_swap

source

theorem equiv.perm.ne_and_ne_of_swap_mul_apply_ne_self {α : Type u} [decidable_eq α] {f : equiv.perm α} {x y : α} (hy : (⇑(equiv.swap x (⇑f x)) * f) y ≠ y) :

⇑f y ≠ y ∧ y ≠ x

source

theorem equiv.perm.support_swap_mul_eq {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} (hffx : ⇑f (⇑f x) ≠ x) :

((equiv.swap x (⇑f x)) * f).support = f.support.erase x

source

theorem equiv.perm.card_support_swap_mul {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} (hx : ⇑f x ≠ x) :

((equiv.swap x (⇑f x)) * f).support.card < f.support.card

source

def equiv.perm.swap_factors_aux {α : Type u} [decidable_eq α] (l : list α) (f : equiv.perm α) (a : ∀ {x : α}, ⇑f x ≠ x → x ∈ l) :

{l // l.prod = f ∧ ∀ (g : equiv.perm α), g ∈ l → g.is_swap}

Equations

equiv.perm.swap_factors_aux (x :: l) = λ (f : equiv.perm α) (h : ∀ {x_1 : α}, ⇑f x_1 ≠ x_1 → x_1 ∈ x :: l), dite (x = ⇑f x) (λ (hfx : x = ⇑f x), equiv.perm.swap_factors_aux l f _) (λ (hfx : ¬x = ⇑f x), let m : {l // l.prod = (equiv.swap x (⇑f x)) * f ∧ ∀ (g : equiv.perm α), g ∈ l → g.is_swap} := equiv.perm.swap_factors_aux l ((equiv.swap x (⇑f x)) * f) _ in ⟨equiv.swap x (⇑f x) :: m.val, _⟩)
equiv.perm.swap_factors_aux list.nil = λ (f : equiv.perm α) (h : ∀ {x : α}, ⇑f x ≠ x → x ∈ list.nil), ⟨list.nil (equiv.perm α), _⟩

source

def equiv.perm.swap_factors {α : Type u} [decidable_eq α] [fintype α] [decidable_linear_order α] (f : equiv.perm α) :

{l // l.prod = f ∧ ∀ (g : equiv.perm α), g ∈ l → g.is_swap}

swap_factors represents a permutation as a product of a list of transpositions. The representation is non unique and depends on the linear order structure. For types without linear order trunc_swap_factors can be used

Equations

f.swap_factors = equiv.perm.swap_factors_aux (finset.sort has_le.le finset.univ) f _

source

def equiv.perm.trunc_swap_factors {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) :

trunc {l // l.prod = f ∧ ∀ (g : equiv.perm α), g ∈ l → g.is_swap}

Equations

f.trunc_swap_factors = quotient.rec_on_subsingleton finset.univ.val (λ (l : list α) (h : ∀ (x : α), ⇑f x ≠ x → x ∈ ⟦l⟧), trunc.mk (equiv.perm.swap_factors_aux l f h)) _

source

theorem equiv.perm.swap_induction_on {α : Type u} [decidable_eq α] [fintype α] {P : equiv.perm α → Prop} (f : equiv.perm α) (a : P 1) (a_1 : ∀ (f : equiv.perm α) (x y : α), x ≠ y → P f → P ((equiv.swap x y) * f)) :

P f

source

theorem equiv.perm.swap_mul_swap_mul_swap {α : Type u} [decidable_eq α] {x y z : α} (hwz : x ≠ y) (hxz : x ≠ z) :

((equiv.swap y z) * equiv.swap x y) * equiv.swap y z = equiv.swap z x

source

theorem equiv.perm.is_conj_swap {α : Type u} [decidable_eq α] {w x y z : α} (hwx : w ≠ x) (hyz : y ≠ z) :

is_conj (equiv.swap w x) (equiv.swap y z)

source

def equiv.perm.fin_pairs_lt (n : ℕ) :

finset (Σ (a : fin n), fin n)

set of all pairs (⟨a, b⟩ : Σ a : fin n, fin n) such that b < a

Equations

equiv.perm.fin_pairs_lt n = finset.univ.sigma (λ (a : fin n), (finset.range ↑a).attach_fin _)

source

theorem equiv.perm.mem_fin_pairs_lt {n : ℕ} {a : Σ (a : fin n), fin n} :

a ∈ equiv.perm.fin_pairs_lt n ↔ a.snd < a.fst

source

def equiv.perm.sign_aux {n : ℕ} (a : equiv.perm (fin n)) :

units ℤ

Equations

a.sign_aux = ∏ (x : Σ (a : fin n), fin n) in equiv.perm.fin_pairs_lt n, ite (⇑a x.fst ≤ ⇑a x.snd) (-1) 1

source

@[simp]

theorem equiv.perm.sign_aux_one (n : ℕ) :

1.sign_aux = 1

source

def equiv.perm.sign_bij_aux {n : ℕ} (f : equiv.perm (fin n)) (a : Σ (a : fin n), fin n) :

Σ (a : fin n), fin n

Equations

f.sign_bij_aux a = dite (⇑f a.snd < ⇑f a.fst) (λ (hxa : ⇑f a.snd < ⇑f a.fst), ⟨⇑f a.fst, ⇑f a.snd⟩) (λ (hxa : ¬⇑f a.snd < ⇑f a.fst), ⟨⇑f a.snd, ⇑f a.fst⟩)

source

theorem equiv.perm.sign_bij_aux_inj {n : ℕ} {f : equiv.perm (fin n)} (a b : Σ (a : fin n), fin n) (a_1 : a ∈ equiv.perm.fin_pairs_lt n) (a_2 : b ∈ equiv.perm.fin_pairs_lt n) (a_3 : f.sign_bij_aux a = f.sign_bij_aux b) :

a = b

source

theorem equiv.perm.sign_bij_aux_surj {n : ℕ} {f : equiv.perm (fin n)} (a : Σ (a : fin n), fin n) (H : a ∈ equiv.perm.fin_pairs_lt n) :

∃ (b : Σ (a : fin n), fin n) (H : b ∈ equiv.perm.fin_pairs_lt n), a = f.sign_bij_aux b

source

theorem equiv.perm.sign_bij_aux_mem {n : ℕ} {f : equiv.perm (fin n)} (a : Σ (a : fin n), fin n) (a_1 : a ∈ equiv.perm.fin_pairs_lt n) :

f.sign_bij_aux a ∈ equiv.perm.fin_pairs_lt n

source

@[simp]

theorem equiv.perm.sign_aux_inv {n : ℕ} (f : equiv.perm (fin n)) :

f⁻¹.sign_aux = f.sign_aux

source

theorem equiv.perm.sign_aux_mul {n : ℕ} (f g : equiv.perm (fin n)) :

(f * g).sign_aux = (f.sign_aux) * g.sign_aux

source

theorem equiv.perm.sign_aux_swap {n : ℕ} {x y : fin n} (hxy : x ≠ y) :

(equiv.swap x y).sign_aux = -1

source

def equiv.perm.sign_aux2 {α : Type u} [decidable_eq α] (a : list α) (a_1 : equiv.perm α) :

units ℤ

Equations

equiv.perm.sign_aux2 (x :: l) f = ite (x = ⇑f x) (equiv.perm.sign_aux2 l f) (-equiv.perm.sign_aux2 l ((equiv.swap x (⇑f x)) * f))
equiv.perm.sign_aux2 list.nil f = 1

source

theorem equiv.perm.sign_aux_eq_sign_aux2 {α : Type u} [decidable_eq α] {n : ℕ} (l : list α) (f : equiv.perm α) (e : α ≃ fin n) (h : ∀ (x : α), ⇑f x ≠ x → x ∈ l) :

equiv.perm.sign_aux ((e.symm.trans f).trans e) = equiv.perm.sign_aux2 l f

source

def equiv.perm.sign_aux3 {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) {s : multiset α} (a : ∀ (x : α), x ∈ s) :

units ℤ

Equations

f.sign_aux3 = quotient.hrec_on s (λ (l : list α) (h : ∀ (x : α), x ∈ ⟦l⟧), equiv.perm.sign_aux2 l f) _

source

theorem equiv.perm.sign_aux3_mul_and_swap {α : Type u} [decidable_eq α] [fintype α] (f g : equiv.perm α) (s : multiset α) (hs : ∀ (x : α), x ∈ s) :

(f * g).sign_aux3 hs = (f.sign_aux3 hs) * g.sign_aux3 hs ∧ ∀ (x y : α), x ≠ y → (equiv.swap x y).sign_aux3 hs = -1

source

def equiv.perm.sign {α : Type u} [decidable_eq α] [fintype α] :

equiv.perm α →* units ℤ

sign of a permutation returns the signature or parity of a permutation, 1 for even permutations, -1 for odd permutations. It is the unique surjective group homomorphism from perm α to the group with two elements.

Equations

equiv.perm.sign = monoid_hom.mk' (λ (f : equiv.perm α), f.sign_aux3 finset.mem_univ) equiv.perm.sign._proof_1

source

@[simp]

theorem equiv.perm.sign_mul {α : Type u} [decidable_eq α] [fintype α] (f g : equiv.perm α) :

⇑equiv.perm.sign (f * g) = (⇑equiv.perm.sign f) * ⇑equiv.perm.sign g

source

@[simp]

theorem equiv.perm.sign_one {α : Type u} [decidable_eq α] [fintype α] :

⇑equiv.perm.sign 1 = 1

source

@[simp]

theorem equiv.perm.sign_refl {α : Type u} [decidable_eq α] [fintype α] :

⇑equiv.perm.sign (equiv.refl α) = 1

source

@[simp]

theorem equiv.perm.sign_inv {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) :

⇑equiv.perm.sign f⁻¹ = ⇑equiv.perm.sign f

source

theorem equiv.perm.sign_swap {α : Type u} [decidable_eq α] [fintype α] {x y : α} (h : x ≠ y) :

⇑equiv.perm.sign (equiv.swap x y) = -1

source

@[simp]

theorem equiv.perm.sign_swap' {α : Type u} [decidable_eq α] [fintype α] {x y : α} :

⇑equiv.perm.sign (equiv.swap x y) = ite (x = y) 1 (-1)

source

theorem equiv.perm.sign_eq_of_is_swap {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f.is_swap) :

⇑equiv.perm.sign f = -1

source

theorem equiv.perm.sign_aux3_symm_trans_trans {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (f : equiv.perm α) (e : α ≃ β) {s : multiset α} {t : multiset β} (hs : ∀ (x : α), x ∈ s) (ht : ∀ (x : β), x ∈ t) :

equiv.perm.sign_aux3 ((e.symm.trans f).trans e) ht = f.sign_aux3 hs

source

theorem equiv.perm.sign_symm_trans_trans {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (f : equiv.perm α) (e : α ≃ β) :

⇑equiv.perm.sign ((e.symm.trans f).trans e) = ⇑equiv.perm.sign f

source

theorem equiv.perm.sign_prod_list_swap {α : Type u} [decidable_eq α] [fintype α] {l : list (equiv.perm α)} (hl : ∀ (g : equiv.perm α), g ∈ l → g.is_swap) :

⇑equiv.perm.sign l.prod = (-1) ^ l.length

source

theorem equiv.perm.sign_surjective {α : Type u} [decidable_eq α] [fintype α] (hα : 1 < fintype.card α) :

function.surjective ⇑equiv.perm.sign

source

theorem equiv.perm.eq_sign_of_surjective_hom {α : Type u} [decidable_eq α] [fintype α] {s : equiv.perm α →* units ℤ} (hs : function.surjective ⇑s) :

s = equiv.perm.sign

source

theorem equiv.perm.sign_subtype_perm {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) {p : α → Prop} [decidable_pred p] (h₁ : ∀ (x : α), p x ↔ p (⇑f x)) (h₂ : ∀ (x : α), ⇑f x ≠ x → p x) :

⇑equiv.perm.sign (f.subtype_perm h₁) = ⇑equiv.perm.sign f

source

@[simp]

theorem equiv.perm.sign_of_subtype {α : Type u} [decidable_eq α] [fintype α] {p : α → Prop} [decidable_pred p] (f : equiv.perm (subtype p)) :

⇑equiv.perm.sign (⇑equiv.perm.of_subtype f) = ⇑equiv.perm.sign f

source

theorem equiv.perm.sign_eq_sign_of_equiv {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (f : equiv.perm α) (g : equiv.perm β) (e : α ≃ β) (h : ∀ (x : α), ⇑e (⇑f x) = ⇑g (⇑e x)) :

⇑equiv.perm.sign f = ⇑equiv.perm.sign g

source

theorem equiv.perm.sign_bij {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] {f : equiv.perm α} {g : equiv.perm β} (i : Π (x : α), ⇑f x ≠ x → β) (h : ∀ (x : α) (hx : ⇑f x ≠ x) (hx' : ⇑f (⇑f x) ≠ ⇑f x), i (⇑f x) hx' = ⇑g (i x hx)) (hi : ∀ (x₁ x₂ : α) (hx₁ : ⇑f x₁ ≠ x₁) (hx₂ : ⇑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂) (hg : ∀ (y : β), ⇑g y ≠ y → (∃ (x : α) (hx : ⇑f x ≠ x), i x hx = y)) :

⇑equiv.perm.sign f = ⇑equiv.perm.sign g

source

def equiv.perm.is_cycle {β : Type v} (f : equiv.perm β) :

Prop

Equations

f.is_cycle = ∃ (x : β), ⇑f x ≠ x ∧ ∀ (y : β), ⇑f y ≠ y → (∃ (i : ℤ), ⇑(f ^ i) x = y)

source

theorem equiv.perm.is_cycle_swap {α : Type u} [decidable_eq α] [fintype α] {x y : α} (hxy : x ≠ y) :

(equiv.swap x y).is_cycle

source

theorem equiv.perm.is_cycle_inv {β : Type v} {f : equiv.perm β} (hf : f.is_cycle) :

f⁻¹.is_cycle

source

theorem equiv.perm.exists_gpow_eq_of_is_cycle {β : Type v} {f : equiv.perm β} (hf : f.is_cycle) {x y : β} (hx : ⇑f x ≠ x) (hy : ⇑f y ≠ y) :

∃ (i : ℤ), ⇑(f ^ i) x = y

source

theorem equiv.perm.is_cycle_swap_mul_aux₁ {α : Type u} [decidable_eq α] [fintype α] (n : ℕ) {b x : α} {f : equiv.perm α} (hb : (⇑(equiv.swap x (⇑f x)) * f) b ≠ b) (h : ⇑(f ^ n) (⇑f x) = b) :

∃ (i : ℤ), ⇑(((equiv.swap x (⇑f x)) * f) ^ i) (⇑f x) = b

source

theorem equiv.perm.is_cycle_swap_mul_aux₂ {α : Type u} [decidable_eq α] [fintype α] (n : ℤ) {b x : α} {f : equiv.perm α} (hb : (⇑(equiv.swap x (⇑f x)) * f) b ≠ b) (h : ⇑(f ^ n) (⇑f x) = b) :

∃ (i : ℤ), ⇑(((equiv.swap x (⇑f x)) * f) ^ i) (⇑f x) = b

source

theorem equiv.perm.eq_swap_of_is_cycle_of_apply_apply_eq_self {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} (hfx : ⇑f x ≠ x) (hffx : ⇑f (⇑f x) = x) :

f = equiv.swap x (⇑f x)

source

theorem equiv.perm.is_cycle_swap_mul {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} (hx : ⇑f x ≠ x) (hffx : ⇑f (⇑f x) ≠ x) :

((equiv.swap x (⇑f x)) * f).is_cycle

source

@[simp]

theorem equiv.perm.support_swap {α : Type u} [decidable_eq α] [_inst_2 _inst_3 : fintype α] {x y : α} (hxy : x ≠ y) :

(equiv.swap x y).support = {x, y}

source

theorem equiv.perm.card_support_swap {α : Type u} [decidable_eq α] [_inst_2 _inst_3 : fintype α] {x y : α} (hxy : x ≠ y) :

(equiv.swap x y).support.card = 2

source

theorem equiv.perm.sign_cycle {α : Type u} [decidable_eq α] [_inst_2 _inst_3 : fintype α] {f : equiv.perm α} (hf : f.is_cycle) :

⇑equiv.perm.sign f = -(-1) ^ f.support.card