ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17

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.

The four isomorphism types of groups of order $30$

Example

Up to isomorphism, the groups of order $30$ are the four semidirect products $C_{15} ⋊ C_{2}$ in which the involution acts trivially, by inversion on both prime factors, by inversion on $C_{3}$ only, or by inversion on $C_{5}$ only. See Every group of order $30$ has normal Sylow $3$ - and $5$ -subgroups and is not simple.

Facts & Assumptions

Given: The hypotheses and objects in the Example.

[L1]

Every group of order $30$ has normal Sylow $3$ - and $5$ -subgroups and is not simple. (Every group of order $30$ has normal Sylow $3$ - and $5$ -subgroups and is not simple).

[L2]

Let $p < q$ be primes. - If $p ∤ (q - 1)$ , every group of order $p q$ is cyclic. - If $p ∣ (q - 1)$ , there are exactly two isomorphism classes of groups of order $p q$ : the cyclic group $C_{p q}$ and one nonabelian semidirect product $C_{q} ⋊ C_{p}$ . (Classification of groups of order $p q$ for primes $p < q$ ).

[L3]

Let $α, β : H \to Aut (N)$ be actions. If $u \in Aut (N)$ and $v \in Aut (H)$ satisfy $β_{v (h)} = u α_{h} u^{- 1} (h \in H),$ then $N ⋊_{α} H ≅ N ⋊_{β} H$ . (Actions changed by automorphisms of the kernel and complement give isomorphic semidirect products).

[L4]

Let $N$ and $H$ be groups (def-group), and let $α : H \to Aut (N)$ be an action by automorphisms (def-action-by-automorphisms). The external semidirect product $N ⋊_{α} H$ is the set $N \times H$ with multiplication. ( The external semidirect product $N ⋊_{α} H$ ).

Verification

technique · direct

1.1

The normal Sylow $3$ - and $5$ -subgroups commute and form a cyclic normal subgroup $N ≅ C_{15}$ . A Sylow $2$ -subgroup $C_{2}$ meets $N$ trivially and $N C_{2} = G$ , so $G ≅ C_{15} ⋊ C_{2}$ .

L1L2L3L4givenalgebra

2.1

Under $C_{15} ≅ C_{3} \times C_{5}$ , an involutory automorphism acts independently on the prime factors. Each factor admits either the trivial action or inversion, giving the four actions stated in the Example.

step 1.1givenalgebra

3.1

The corresponding centers have orders $30$ , $1$ , $5$ , and $3$ , respectively, so the groups are pairwise nonisomorphic. Every group of order $30$ arose in step 1.1, proving exhaustiveness. This proves the stated claim.

step 2.1givenalgebra∎

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: 113 results over 18 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, Consequences of the Sylow Theorems, Sections 1-5 (standard reference, not scraped)

The four isomorphism types of groups of order 3030