English
There exists a homomorphism sign: Perm α → ℤˣ sending each permutation to its sign, such that sign is a surjective monoid homomorphism.
Русский
Существует гомоморфизм sign: Perm α → ℤˣ, отправляющий каждую перестановку в ее знак, и sign является сюръективной гомоморфизмом моноида.
LaTeX
$$$\mathrm{sign}: \mathrm{Perm}(\alpha) \to \mathbb{Z}^\times$ является моноид-гомоморфизм и сюръективен$$
Lean4
/-- `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. -/
def sign [Fintype α] : Perm α →* ℤˣ :=
MonoidHom.mk' (fun f => signAux3 f mem_univ) fun f g => (signAux3_mul_and_swap f g _ mem_univ).1
