ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

The Frattini subgroup of $(Z / p)^{n}$ is trivial

Example

For every prime $p$ and $n \in N$ , $Φ ((Z / p)^{n}) = 1$ and the generator rank is $n$ .

Facts & Assumptions

Given: A prime $p$ and a natural number $n$ .

[L1]

A finite $p$ -group has trivial Frattini subgroup if and only if it is elementary abelian (A finite $p$ -group has trivial Frattini subgroup exactly when it is elementary abelian).

[F1]

A basis of an elementary abelian $p$ -group is an independent spanning subset for its canonical $F_{p}$ -linear structure ( $F_{p}$ -spanning sets, independence, and bases in an elementary abelian $p$ -group).

[L2]

The quotient $Z / p$ has $p$ elements, is a field, and a finite Cartesian product has the product cardinality (For $n \geq 1$ , every class in $Z / n$ has one representative $r$ with $0 \leq r < n$ , so $∣ Z / n ∣ = n$ ; while $Z / 0$ is in bijection with $Z$ , For every prime $p$ , the two operations on $Z / p$ make it a field, The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ).

[F2]

The generator rank $d (P)$ is the common size of a basis of $P / Φ (P)$ (The generator rank $d (P)$ of a finite $p$ -group).

Verification

technique · direct

1.1

Componentwise addition makes $(Z / p)^{n}$ a finite abelian group of order $p^{n}$ by [L2], and every nonzero element has order $p$ . It is therefore elementary abelian and [L1] gives $Φ ((Z / p)^{n}) = 1$ . At $n = 0$ , the empty product is the trivial group and the same conclusion holds.

givenL1L2algebra

2.1

The standard coordinate vectors have unique coordinates, so they form a basis by [F1]. There are $n$ of them, hence [F2] gives $d ((Z / p)^{n}) = n$ , including the empty basis at $n = 0$ .

step 1.1F1F2L2algebra∎

Depends on

Used by

FALSE: the Frattini subgroup is the union of the maximal subgroups False statement

Dependency tree · two levels

31 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

D. A. Craven, The Theory of p-Groups, Definition 2.6 (standard reference, not scraped)
K. Conrad, Generating Sets, §6 (standard reference, not scraped)

The Frattini subgroup of (Z/p)n(Z/p)n is trivial