alternatingGroup — Mathlib

English

The alternating group on α is the kernel of the sign homomorphism from the permutation group on α to {±1}.

Русский

Чередующаяся группа на α есть ядро гомоморфизма знака из симметрической группы на α в {±1}.

LaTeX

$$$\mathrm{alternatingGroup}(\alpha) = \ker(\mathrm{sign})$$$

Lean4

/-- The alternating group on a finite type, realized as a subgroup of `Equiv.Perm`.
  For $A_n$, use `alternatingGroup (Fin n)`. -/
def alternatingGroup : Subgroup (Perm α) :=
  sign.ker

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