LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedaudited 2026-09-06

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.

Hyperelementary permutation subring reduction

Statement

Let $H^{'}$ be the $p$ -hyperelementary subgroups of $G$ , for all primes $p$ . The additive span $P (H^{'}) = \sum_{H \in H^{'}} Z {Ind}_{H}^{G} 1_{H}$ is a subring of $R (G)$ . Moreover, if $1_{G} \in P (H^{'})$ , then proving $1_{H} \in I_{E} (H)$ for each hyperelementary $H$ implies $1_{G} \in I_{E} (G)$ .

Facts & Assumptions

[F1]

The cited prerequisite is Mackey's double-coset formula for restricting an induced character.

Proof

Given: $H, K \in H^{'}$ and $E$ is the elementary family.

1.1

Mackey's formula expresses ${Res}_{H}^{G} {Ind}_{K}^{G} 1_{K}$ as a sum of permutation characters induced from $H \cap x K x^{- 1}$ . Those intersections are hyperelementary by subgroup closure, and induction back to $G$ shows that products of the displayed generators stay in $P (H^{'})$ .

F1given

2.1

If $1_{H} \in I_{E} (H)$ , transitivity puts ${Ind}_{H}^{G} 1_{H}$ in $I_{E} (G)$ . Apply this to every summand of a relation for $1_{G}$ in $P (H^{'})$ . ∎

step 1.1

Depends on

Used by

Banaschewski's prime obstruction Lemma

Dependency tree · two levels

16 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

Wen-Wei Li, Yanqi Lake Lectures on Algebra I, Lemma 14.3.3 (standard reference, not scraped)