CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$A_n$ is normal in $S_n$ ; for $n\ge2$ , $2\,|A_n|=n!$ , while $A_n=S_n$ for $n=0,1$

Statement

For every natural $n$ , $A_n$ is a normal subgroup of $S_n$ . If $n\ge2$ , then $2|A_n|=n!$ . If $n=0$ or $n=1$ , then $A_n=S_n$ .

Facts & Assumptions

Given: A natural $n$ , the sign homomorphism on $S_n$ , and the alternating group $A_n$ .

[L1]

$A_n$ is the kernel of sign (The alternating group $A_n=\ker(\operatorname{sgn})$ of even permutations).

[L2]

The kernel of every group homomorphism is a normal subgroup (The image of a group homomorphism is a subgroup and its kernel is a normal subgroup).

[L3]

The symmetric group of an $n$ -element set has $n!$ elements (A finite set $A$ with $\lvert A\rvert = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality).

[L4]

Sign is a homomorphism whose image is $\{+1,-1\}$ exactly when $n\ge2$ , and is $\{1\}$ for $n=0,1$ (The sign is a homomorphism $S_n\to\{+1,-1\}$ , surjective exactly when $n\ge 2$ ).

[L5]

The cardinality of a disjoint union of two finite sets is the sum of their cardinalities (The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , and a sum over a finite index set splits along a partition).

Proof

technique · direct

1.1

By [L1] and [L2], $A_n$ is a normal subgroup of $S_n$ .

givenL1L2

2.1

Suppose $n\ge2$ . By [L4], choose $\tau\in S_n$ with $\operatorname{sgn}(\tau)=-1$ . Left multiplication $\sigma\mapsto\tau\sigma$ is a bijection from the even fibre of sign to the odd fibre, with inverse left multiplication by $\tau^{-1}$ , because [L4] gives $\operatorname{sgn}(\tau\sigma)=-\operatorname{sgn}(\sigma)$ .

step 1.1L1L4

3.1

The even and odd fibres are disjoint and have union $S_n$ , and step 2.1 gives them equal finite cardinality. Thus [L5] and [L3] give $n!=|S_n|=|A_n|+|A_n|=2|A_n|$ .

step 2.1L1L3L5

4.1

If $n=0$ or $n=1$ , [L4] says that sign has image $\{1\}$ , so its kernel is all of $S_n$ and $A_n=S_n$ .

step 3.1L1L4∎

Depends on

Used by

A₄ consists of the identity, eight 3-cycles, and three products of disjoint transpositions Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 97 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

T. W. Judson, Abstract Algebra: Theory and Applications, §5.1, Theorem 5.7 and Proposition 5.8 (standard reference, not scraped)

AnA_nAn​ is normal in SnS_nSn​; for n≥2n\ge2n≥2, 2 ∣An∣=n!2\,|A_n|=n!2∣An​∣=n!, while An=SnA_n=S_nAn​=Sn​ for n=0,1n=0,1n=0,1