LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

P residual is generated by p prime elements and idempotent

Statement

Let $G$ be a finite group and let $p$ be a prime. Then:

$O^{p} (G)$ is generated by the set of $p^{'}$ -elements of $G$ ;
$G = P O^{p} (G)$ for every Sylow $p$ -subgroup $P$ of $G$ ;
$O^{p} (O^{p} (G)) = O^{p} (G)$ .

Facts & Assumptions

Given: A finite group $G$ , a prime $p$ , and the $p$ -residual $O^{p} (G)$ of P residual of a finite group; $p^{'}$ -elements are as in The p-prime core of a finite group.

[F1]

$O^{p} (G) ⊴ G$ , $G / O^{p} (G)$ is a finite $p$ -group, and $O^{p} (G)$ is the least normal subgroup of $G$ with $p$ -group quotient (P residual of a finite group, Normal subgroup: invariance under conjugation).

[F2]

If $θ : G \to A$ is a homomorphism into a finite $p$ -group $A$ and $x \in G$ is a $p^{'}$ -element, then $θ (x) = e$ : $ord (θ (x))$ divides $ord (x)$ and divides $∣ A ∣$ , hence is both prime to $p$ and a power of $p$ , so equals $1$ (If $ord (g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$ , the powers $g^{0}, \dots, g^{n - 1}$ are distinct, and $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ , A group homomorphism automatically satisfies $f (e) = e^{'}$ and $f (g^{- 1}) = f (g)^{- 1}$ , and $f (g^{n}) = f (g)^{n}$ for every $n \in Z$ ; for monoid homomorphisms preservation of the identity must be assumed, The order of every element of a finite group divides the order of the group, The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity, The $p$ -adic valuation $v_{p} (a)$ of a nonzero integer: the greatest $k \in N$ with $p^{k} ∣ a$ ).

[F3]

By Sylow subgroups of a normal subgroup are intersections with Sylow subgroups applied to the normal subgroup $O^{p} (G)$ and a Sylow $P$ of $G$ : $P \cap O^{p} (G) \in {Syl}_{p} (O^{p} (G))$ and $G = P O^{p} (G)$ , since $[G : O^{p} (G)]$ is a power of $p$ by [F1] (Sylow I: every finite group has a Sylow $p$ -subgroup, Sylow $p$ -subgroups of a finite group).

[F4]

If a prime $ℓ$ divides the order of a finite group $H$ , then $H$ has an element of order $ℓ$ (Cauchy's theorem: if a prime $p$ divides $∣ G ∣$ , then $G$ has an element of order $p$ ).

[F5]

The subgroup generated by a set $Y$ consists of finite products of elements of $Y$ and their inverses; conjugation is an automorphism, so $g ⟨ Y ⟩ g^{- 1} = ⟨ g Y g^{- 1} ⟩$ (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups, Conjugation $x \mapsto g x g^{- 1}$ is an automorphism, A group homomorphism automatically satisfies $f (e) = e^{'}$ and $f (g^{- 1}) = f (g)^{- 1}$ , and $f (g^{n}) = f (g)^{n}$ for every $n \in Z$ ; for monoid homomorphisms preservation of the identity must be assumed).

[F6]

$G / R$ is a finite $p$ -group if and only if $[G : R]$ is a power of $p$ ; if $[G : R]$ has a prime divisor $ℓ$ , then $ℓ \neq p$ means $G / R$ is not a $p$ -group; and $x^{k} = e$ implies $(x^{k})^{j} = e$ for every $j$ (If $[G : N]$ is finite then $∣ G / N ∣ = [G : N]$ ; for finite $G$ this equals $∣ G ∣ / ∣ N ∣$ , A finite $p$ -group has order $p^{n}$ for a prime $p$ and some $n \in N$ , Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime, Divisibility is reflexive and transitive on $Z$ , and is linear: if $d ∣ a$ and $d ∣ b$ then $d ∣ a x + b y$ for all integers $x, y$ ; also $d ∣ a$ implies $d ∣ a c$ , $- d ∣ a$ and $d ∣ - a$ , The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity).

[F7]

$ord (x^{- 1}) = ord (x)$ , and conjugation preserves orders (If $ord (g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$ , the powers $g^{0}, \dots, g^{n - 1}$ are distinct, and $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ , Conjugation $x \mapsto g x g^{- 1}$ is an automorphism).

Proof

technique · direct

1.1

Let $Y$ be the set of $p^{'}$ -elements of $G$ and let $R : = ⟨ Y ⟩$ . Then $R ⊴ G$ : if $y \in Y$ then every conjugate $g y g^{- 1}$ is again a $p^{'}$ -element by [F7], so $g Y g^{- 1} = Y$ and hence $g R g^{- 1} = R$ by [F5].

F5F7algebra

1.2

$G / R$ is a $p$ -group. Suppose not; then by [F6] some prime $q \neq p$ divides $[G : R]$ , so $G / R$ has an element $y R$ of order $q$ by [F4]. Let $ord (y) = p^{s} e$ with $p ∤ e$ ([F1] of The $p$ -adic valuation $v_{p} (a)$ of a nonzero integer: the greatest $k \in N$ with $p^{k} ∣ a$ ); then $(y^{p^{s}})^{e} = y^{ord (y)} = e$ , so $y^{p^{s}}$ has order dividing $e$ and is therefore a $p^{'}$ -element, that is, $y^{p^{s}} \in Y \subseteq R$ by [F6]. Hence $(y R)^{p^{s}} = R$ , so the order of $y R$ divides $p^{s}$ ; but that order is $q$ , a prime different from $p$ , a contradiction.

F4F5F6algebra

1.3

Claim 2 is exactly the second assertion of [F3].

2.1

Therefore $O^{p} (G) \leq R$ : $R$ is a normal subgroup of $G$ with $p$ -group quotient by steps 1.1 and 1.2, and $O^{p} (G)$ is the least such by [F1].

F1step 1.1step 1.2

3.1

Conversely $Y \subseteq O^{p} (G)$ : the natural map $G \to G / O^{p} (G)$ is a homomorphism onto a finite $p$ -group by [F1], so it kills every $p^{'}$ -element by [F2]. Hence $R = ⟨ Y ⟩ \subseteq O^{p} (G)$ , and with step 2.1, $R = O^{p} (G)$ ; this is claim 1.

F1F2step 2.1

4.1

Claim 3: put $K : = O^{p} (G)$ . By claim 1 applied to the finite group $K$ , $O^{p} (K)$ is generated by the $p^{'}$ -elements of $K$ ; every such element is a $p^{'}$ -element of $G$ and so lies in $K$ trivially, while conversely claim 1 gives $K = ⟨ Y ⟩$ with $Y$ the $p^{'}$ -elements of $G$ , and every $y \in Y$ is an element of $K$ and hence a $p^{'}$ -element of $K$ . The two generating sets agree, so $O^{p} (K) = K$ . ∎

step 3.1algebra

Depends on

Used by

Dependency tree · two levels

93 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

Paul Flavell, An Introduction to Transfer and Fusion in Finite Groups, §§2–5 (standard reference, not scraped)