ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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.1L1L2L3L4givenalgebra

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

2.1step 1.1givenalgebra

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.

3.1step 2.1givenalgebra∎

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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, Consequences of the Sylow Theorems, Sections 1-5 (standard reference, not scraped)

The four isomorphism types of groups of order 3030