LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

$p$ -primary congruence for integer-valued cyclotomic character combinations

Statement

Let $A = Z [ζ_{∣ G ∣}]$ , and let $A R (G)$ denote the $A$ -span of the complex characters of $G$ . If $χ \in A R (G)$ is integer-valued, $g \in G$ , and $g = g_{p} g_{p^{'}}$ is its commuting $p$ -part/ $p^{'}$ -part decomposition, then

$χ (g) \equiv χ (g_{p^{'}}) (m o d p) .$

Facts & Assumptions

[F1]

The cited prerequisite is Every irreducible representation of a finite abelian group over a splitting field is one-dimensional.

Proof

Given: $∣ g ∣ = p^{n} l$ with $(p, l) = 1$ , and $g_{p^{'}} = g^{p^{n} a}$ for $a p^{n} \equiv 1 (m o d l)$ .

1.1

On the cyclic group $⟨ g ⟩$ , every irreducible complex character is linear. For each such character $ψ$ , the $p^{n}$ -th powers of $ψ (g)$ and $ψ (g_{p^{'}})$ agree, since $g^{p^{n}} = g_{p^{'}}^{p^{n}}$ .

F1given

2.1

Write the restriction as $\sum_{i} a_{i} ψ_{i}$ with $a_{i} \in A$ and the $ψ_{i}$ linear. In $A / p A$ , the freshman's dream and step 1.1 give the following congruence.

step 1.1algebra

$χ (g)^{p^{n}} - χ (g_{p^{'}})^{p^{n}} \equiv \sum_{i} a_{i}^{p^{n}} (ψ_{i} (g)^{p^{n}} - ψ_{i} (g_{p^{'}})^{p^{n}}) = 0.$

3.1

Both character values are integers. The power basis $1, ζ_{∣ G ∣}, \dots, ζ_{∣ G ∣}^{φ (∣ G ∣) - 1}$ makes $Z \cdot 1$ a direct summand of $A$ , so $p A \cap Z = p Z$ . Fermat's congruence then gives $χ (g) \equiv χ (g)^{p^{n}} \equiv χ (g_{p^{'}})^{p^{n}} \equiv χ (g_{p^{'}}) (m o d p)$ . ∎

step 2.1algebra

Depends on

Used by

Elementary detection at a fixed element Lemma

Dependency tree · two levels

13 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

János Kramár, Artin's and Brauer's Theorems on Induced Characters, Lemma 4 (standard reference, not scraped)

pp-primary congruence for integer-valued cyclotomic character combinations