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.

Sylow data for finite groups of order at most $15$

Example

For finite groups of positive order at most $15$ , the Sylow subgroup orders and possible counts are as follows. An entry $p^{a} : n_{p}$ gives the Sylow order and the permitted values of its count.

$\begin{array}{cll} ∣ G ∣ & Sylow data & forced normal Sylow subgroups \\ 1 & none & none \\ 2 & 2 : 1 & 2 \\ 3 & 3 : 1 & 3 \\ 4 & 4 : 1 & 4 \\ 5 & 5 : 1 & 5 \\ 6 & 2 : 1 or 3, 3 : 1 & 3 \\ 7 & 7 : 1 & 7 \\ 8 & 8 : 1 & 8 \\ 9 & 9 : 1 & 9 \\ 10 & 2 : 1 or 5, 5 : 1 & 5 \\ 11 & 11 : 1 & 11 \\ 12 & 4 : 1 or 3, 3 : 1 or 4 & none from the numerical restrictions alone \\ 13 & 13 : 1 & 13 \\ 14 & 2 : 1 or 7, 7 : 1 & 7 \\ 15 & 3 : 1, 5 : 1 & 3, 5 \end{array}$

The order- $15$ entry also uses the order- $p q$ classification; no classification at orders $8$ or $12$ is asserted. See Sylow I: every finite group has a Sylow $p$ -subgroup.

Facts & Assumptions

Given: The hypotheses and objects in the Example.

[L1]

Let $G$ be finite, let $p$ be prime, and write $∣ G ∣ = p^{a} m$ with $p ∤ m$ . Then $G$ has a subgroup of order $p^{a}$ , hence a Sylow $p$ -subgroup (def-sylow-p-subgroup). (Sylow I: every finite group has a Sylow $p$ -subgroup).

[L2]

Let $∣ G ∣ = p^{a} m$ with $p ∤ m$ . Then the number of Sylow $p$ -subgroups satisfies $n_{p} (G) \equiv 1 (m o d p), n_{p} (G) ∣ m .$ . (Sylow III: $n_{p} \equiv 1 (m o d p)$ and $n_{p} ∣ m$ when $∣ G ∣ = p^{a} m$ with $p ∤ m$ ).

[L3]

A Sylow $p$ -subgroup of a finite group is normal if and only if it is the unique Sylow $p$ -subgroup. (A Sylow $p$ -subgroup is normal if and only if it is unique).

[L4]

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

[L5]

Every finite $p$ -group is nilpotent. The trivial group is included and has nilpotency class zero. (Every finite $p$ -group is nilpotent).

Verification

technique · direct

1.1

Factoring each order and applying $n_{p} ∣ ∣ G ∣ / p^{a}$ together with $n_{p} \equiv 1 (m o d p)$ gives every entry through order $14$ , including the two independent possibilities displayed at order $12$ .

L1L2L3L4L5givenalgebra

2.1

At order $15$ , Sylow III forces $n_{5} = 1$ , while the order- $p q$ classification makes the group cyclic and hence also gives $n_{3} = 1$ . The entries at orders $8$ and $12$ record only Sylow data, not isomorphism types.

step 1.1givenalgebra

3.1

At order $1$ no prime divides the group order, so there is no Sylow subgroup to list. 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: 127 results over 20 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)

Sylow data for finite groups of order at most 1515