LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Isaacs' linear-character step

Statement

Suppose $G = N ⋊ P$ , where $N$ has order prime to $p$ and $P$ is a $p$ -group. If a linear character $λ : N \to C^{\times}$ is $P$ -invariant and $C_{N} (P) \subseteq \ker λ$ , then $λ = 1_{N}$ .

Facts & Assumptions

[F1]

The cited prerequisite is If a finite $p$ -group $P$ acts on a finite set $X$ , then $∣ X ∣ \equiv ∣ X^{P} ∣ (m o d p)$ .

Proof

Given: $ν \in N$ and $P$ acts on the fibre $λ^{- 1} (λ (ν))$ by conjugation.

1.1F1given

The fibre is $P$ -stable by invariance and has cardinality $∣ \ker λ ∣$ , a divisor of $∣ N ∣$ and hence prime to $p$ . The fixed-point congruence supplies a $P$ -fixed element in that fibre.

2.1step 1.1

A fixed element lies in $C_{N} (P) \subseteq \ker λ$ , so its character value is $1$ . Since the fibre has that same value, $λ (ν) = 1$ ; as $ν$ was arbitrary, $λ$ is trivial. ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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.6 (standard reference, not scraped)