ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-16

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.

$S_{3} ≅ C_{3} ⋊ C_{2}$ via inversion

Example

The symmetric group on three letters satisfies

$S_{3} ≅ C_{3} ⋊ C_{2},$

where the nonidentity element of $C_{2}$ acts on $C_{3}$ by inversion.

Facts & Assumptions

Given: In $S_{3}$ , let $r = (123)$ and $s = (12)$ .

[L1]

Normal subgroups $N, H$ satisfying $G = N H$ and $N \cap H = 1$ realise the corresponding external semidirect product ( Recognition theorem: $G = N H$ with $N ⊴ G$ , $N \cap H = 1$ exactly realises an external semidirect product).

[L2]

For $n \geq 1$ the dihedral group $D_{n}$ is $Dih (C_{n}) = C_{n} ⋊ C_{2}$ with inversion action, of order $2 n$ ( $Dih (C_{n}) = C_{n} ⋊ C_{2}$ with inversion action has order $2 n$ and the dihedral relations).

[L3]

$S_{3}$ is the group of permutations of a three-element set (The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition).

Verification

technique · direct

1.1L3algebra

The subgroup $N = ⟨ r ⟩ = {1, (123), (132)}$ has index two in the six-element group $S_{3}$ , and direct conjugation by every permutation preserves the set of the two $3$ -cycles. Hence $N ⊴ S_{3}$ .

1.2L3algebra

The subgroup $H = ⟨ s ⟩$ has order two, intersects $N$ trivially, and the six products $r^{i} s^{j}$ are distinct. Thus $S_{3} = N H$ .

2.1step 1.1step 1.2L1L2algebra∎

Since $s r s^{- 1} = (132) = r^{- 1}$ , [L1] gives the asserted semidirect product, which is the order-six case of [L2].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Keith Conrad, Semidirect Products (standard reference, not scraped)

S3≅C3⋊C2S3​≅C3​⋊C2​ via inversion