Theorems · Definition · group theory

Equiv.Perm.sign

{α : Type u} → [DecidableEq α] → [Fintype α] → Equiv.Perm α →* ℤˣ

SignType.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.

Defined in

Mathlib.GroupTheory.Perm.Sign

Cited by

138 results in Mathlib

Foundations

Depth 77 from the axioms, rests on 1,900 definitions · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintype