index_eq_one — Mathlib

English

For a finite set α, the index of the alternating group on α is 1 when α has only one element (i.e., is a subsingleton).

Русский

Для конечного множества α индекс чередующей группы на α равен 1, если α состоит из одного элемента.

LaTeX

$$$\\text{index} (\\text{alternatingGroup } \\alpha) = 1$ when $|\\alpha|=1$ (i.e., Subsingleton α).$$

Lean4

@[nontriviality]
theorem index_eq_one [Subsingleton α] : (alternatingGroup α).index = 1 := by rw [Subgroup.index_eq_one];
  apply Subsingleton.elim

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