Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13
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.

[Sn,Sn]=An for n≥2, and [An,An]=An for n≥5

Statement

For n≥2, [Sn,Sn]=An. For n≥5, [An,An]=An.

Facts & Assumptions

Given: The groups Sn and An in the stated ranges of n.

[F1]

[G,G] is generated by the commutators [g,h]=ghg−1h−1 (Commutators [g,h]=ghg−1h−1 and the commutator subgroup [G,G]).

[F2]

The commutator subgroup is normal (The commutator subgroup is normal).

[F3]

For N⊴G, the quotient G/N is abelian exactly when [G,G]⊆N (G/N is abelian if and only if [G,G]⊆N).

[F5]

An is simple for n≥5 (An is simple for every n≥5).

Proof

technique · direct
1.1

Since Sn/An is the abelian sign image, [F3] gives [Sn,Sn]⊆An.

F3F4algebra
1.2

Every 3-cycle satisfies (a b c)=[(b c),(a b)] under the convention in [F1], so [F4] gives An⊆[Sn,Sn] for n≥3.

F1F4algebra
1.3

For n≥5, the 3-cycles (1 2 3) and (3 4 5) do not commute, so [An,An] is nontrivial by [F1].

F1algebra
2.1

At n=2, both A2 and the commutator subgroup of the abelian group S2 are trivial. Thus steps 1.1--1.2 prove the first formula for all n≥2.

F1F4step 1.1step 1.2
3.1

This subgroup is normal by [F2], and simplicity [F5] therefore forces [An,An]=An.

F2F5step 1.3∎

Depends on

Used by

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources