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 unique Sylow $p$ -subgroup of $Aff (Z / p^{2})$

Example

For every prime $p$ , the affine group of $Z / p^{2}$ has a unique Sylow $p$ -subgroup, consisting of the maps $x \mapsto a x + b$ with $a \equiv 1 (m o d p)$ . It has order $p^{3}$ , including when $p = 2$ . See Sylow III: $n_{p} \equiv 1 (m o d p)$ and $n_{p} ∣ m$ when $∣ G ∣ = p^{a} m$ with $p ∤ m$ .

Facts & Assumptions

Given: The hypotheses and objects in the Example.

[L1]

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

[L2]

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

[L3]

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

[L4]

For every prime $p$ and natural $k \geq 1$ , $φ (p^{k}) = p^{k} - p^{k - 1} .$ Equivalently, among the $p^{k}$ standard classes modulo $p^{k}$ , the nonunits are exactly those whose standard representatives are divisible by $p$ . (For a prime $p$ and $k \geq 1$ , $φ (p^{k}) = p^{k} - p^{k - 1}$ ).

[L5]

Let $n \geq 1$ and $a \in Z$ . Then $[a]_{n}$ is a unit of $Z / n$ (def-unit-group-modulo-n-and-euler-totient) if and only if $\gcd (a, n) = 1,$ that is, if and only if $a$ and $n$ are coprime (def-coprime). Consequently the condition $\gcd (a, n) = 1$ depends only on the class $[a]_{n}$ . (For $n \geq 1$ , $[a]_{n}$ is a unit if and only if $\gcd (a, n) = 1$ ).

Verification

technique · direct

1.1

The affine group is $(Z / p^{2}) ⋊ (Z / p^{2})^{\times}$ and has order $p^{2} φ (p^{2}) = p^{3} (p - 1)$ . Reduction of the multiplier modulo $p$ is a homomorphism to $(Z / p)^{\times}$ .

L1L2L3L4L5givenalgebra

2.1

Its kernel consists of arbitrary translations and the $p$ units $1 + p t$ with $t \in Z / p$ . It is therefore normal of order $p^{2} \cdot p = p^{3}$ , the full $p$ -part of the affine-group order, and so is the unique Sylow $p$ -subgroup.

step 1.1givenalgebra

3.1

For $p = 2$ , both units modulo $4$ are congruent to $1$ modulo $2$ , so the kernel is the whole affine group of order $8$ ; the same conclusion holds without exception. 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: 100 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 unique Sylow pp-subgroup of Aff⁡(Z/p2)Aff(Z/p2)