sign_of_cycleType' — Mathlib

English

The sign of a permutation σ is the product over its cycle-type components: sign(σ) = ∏_{n ∈ cycleType(σ)} (-1)^{n+1}.

Русский

Знак перестановки σ равен произведению по компонентам её cycle-type: sign(σ) = ∏_{n ∈ cycleType(σ)} (-1)^{n+1}.

LaTeX

$$$$\mathrm{sign}(\sigma) = \prod_{n \in \mathrm{cycleType}(\sigma)} (-1)^{n+1}.$$$$

Lean4

theorem sign_of_cycleType' (σ : Perm α) : sign σ = (σ.cycleType.map fun n => -(-1 : ℤˣ) ^ n).prod := by
  induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => simp [hσ.cycleType, hσ.sign]
  | induction_disjoint σ τ hd _ hσ hτ => simp [hσ, hτ, hd.cycleType_mul]

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