Alternating_Group_is_Normal_Subgroup_of_Symmetric_Group_v2

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

alternating-groupsgroup-theorynormal-subgroupsproofwikisymmetric-groups

Let $n \ge 2$ be a natural number. Let $S_n$ denote the symmetric group on $n$ letters. Let $A_n$ be the alternating group on $n$ letters. Then $A_n$ is a normal subgroup of $S_n$ whose index is $2$ .

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.GroupTheory.Perm.Cycle.Type

Formal statement

theorem Alternating_Group_is_Normal_Subgroup_of_Symmetric_Group_v2 {n : ℕ} : (Equiv.Perm.sign.ker : Subgroup (Equiv.Perm (Fin n))).Normal := by sorry

Source

https://proofwiki.org/wiki/Alternating_Group_is_Normal_Subgroup_of_Symmetric_Group

View graph