English
If f is a cycle, then the sign of f equals -(-1)^{|supp(f)|}, where supp(f) is the set of elements moved by f.
Русский
Пусть f — цикл; знак f равен -(-1)^{|Опора(f)|}, где Опора(f) — множество элементов, смещаемых f.
LaTeX
$$\( \operatorname{sign}(f) = -(-1)^{|\operatorname{supp}(f)|} \quad \text{when } f \text{ is a cycle}.$$
Lean4
theorem sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ #f.support :=
let ⟨x, hx⟩ := hf
calc
Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f)) := by {
rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]
}
_ = -(-1) ^ #f.support :=
if h1 : f (f x) = x then
by
have h : swap x (f x) * f = 1 := by
simp only [mul_def, one_def]
rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]
rw [sign_mul, sign_swap hx.1.symm, h, sign_one, hf.eq_swap_of_apply_apply_eq_self hx.1 h1,
card_support_swap hx.1.symm]
rfl
else
by
have h : #(swap x (f x) * f).support + 1 = #f.support := by
rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1, card_insert_of_notMem (notMem_erase _ _),
sdiff_singleton_eq_erase]
rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h]
simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one]
termination_by #f.support
