sign_of_cycleType — Mathlib

English

The sign of σ is equal to (−1) raised to the power sum of cycle lengths plus their number.

Русский

Знак σ равен (−1) в степени суммы длин циклoв плюс число циклов.

LaTeX

$$$$\mathrm{sign}(\sigma) = (-1)^{\, \sum \mathrm{cycleType}(\sigma) + |\mathrm{cycleType}(\sigma)|}.$$$$

Lean4

theorem sign_of_cycleType (f : Perm α) : sign f = (-1 : ℤˣ) ^ (f.cycleType.sum + Multiset.card f.cycleType) :=
  by
  rw [sign_of_cycleType']
  induction f.cycleType using Multiset.induction_on with
  | empty => rfl
  | cons a s ihs =>
    rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]
    simp only [pow_add, pow_one, neg_mul, mul_neg, mul_assoc, mul_one]

Похожие утверждения