LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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.

A finite product of normal $p$ -subgroups is a normal $p$ -subgroup

Statement

A finite product of normal $p$ -subgroups of a group is a normal $p$ -subgroup. The empty product is the trivial subgroup. See A finite $p$ -group has order $p^{n}$ for a prime $p$ and some $n \in N$ .

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

Let $p$ be a prime natural number (def-prime). A finite $p$ -group is a finite group $P$ (def-group, def-finite-cardinality) whose order has the form $∣ P ∣ = p^{n}$ for some $n \in N$ , with natural exponentiation as in def-nat-power. The case $n = 0$ permits the trivial group. A finite $p$ -group is nontrivial exactly when $n \geq 1$ . (A finite $p$ -group has order $p^{n}$ for a prime $p$ and some $n \in N$ ).

[L2]

If $H \leq G$ and $N ⊴ G$ , then $H N$ is a subgroup and $H \cap N ⊴ H$ . Here $H N : = {h n : h \in H, n \in N}$ . (If $H \leq G$ and $N ⊴ G$ , then $H N$ is a subgroup and $H \cap N ⊴ H$ ).

[L3]

If $H$ is a subgroup of a finite group $G$ , then $∣ G ∣ = [G : H] ∣ H ∣$ ; in particular $∣ H ∣$ divides $∣ G ∣$ . (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

Proof

technique · direct

1.1

Induct on the number of factors; the empty product is the trivial normal $p$ -subgroup.

L1L2givenalgebra

2.1

Let $A$ and $B$ be normal $p$ -subgroups. By [L2], $A B$ is a subgroup, and $g A B g^{- 1} = A B$ for every ambient-group element $g$ , so $A B$ is normal. The multiplication map $A \times B \to A B$ is surjective. For a fixed factorization $a b$ , all its preimages are exactly $(a x, x^{- 1} b)$ with $x \in A \cap B$ . Thus every fibre has $∣ A \cap B ∣$ elements and $∣ A B ∣ = ∣ A ∣ ∣ B ∣ / ∣ A \cap B ∣$ . By [L3], $∣ A \cap B ∣$ is a power of $p$ , so $∣ A B ∣$ is a power of $p$ .

step 1.1L2L3givenalgebra

3.1

Applying step 2.1 repeatedly proves the result for every finite product, including one factor and repeated factors.

step 1.1step 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: 75 results over 16 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, The Sylow Theorems, Sections 1-2 (standard reference, not scraped)

A finite product of normal pp-subgroups is a normal pp-subgroup