ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.1

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}$ .

L3algebra

1.2

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$ .

L3algebra

2.1

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

step 1.1step 1.2L1L2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 39 results over 13 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

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

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