instCharacteristicPermAlternatingGroup

English

The alternating group is a characteristic subgroup of the permutation group.

Русский

Чередующаяся группа является характеристической подгруппой группы перестановок.

LaTeX

$$$$\\operatorname{IsCharacteristic}(\\operatorname{alternatingGroup}(\\alpha), \\operatorname{Perm}(\\alpha)).$$$$

Lean4

/-- The alternating group is a characteristic subgroup of the permutation group. -/
instance : (alternatingGroup α).Characteristic where
  fixed
    φ := by
    nontriviality α
    apply eq_alternatingGroup_of_index_eq_two
    rw [index_comap_of_surjective _ (Equiv.surjective _), alternatingGroup.index_eq_two]

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