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 Fitting and Frattini subgroups of
Example
For , one has , , , and . Hence . See The Fitting subgroup of a finite group.
Facts & Assumptions
Given: The hypotheses and objects in the Example.
For a finite group , the Fitting subgroup is the product of its -cores (def-p-core-of-a-finite-group). The factors are normal, so their finite product is a normal subgroup and does not depend on the order of multiplication. For the trivial group the product is empty and equals . (The Fitting subgroup of a finite group).
For a finite group , the Frattini subgroup is If , the family is empty and its intersection inside is itself. Thus . (The Frattini subgroup as the intersection of the maximal subgroups of a finite group).
For every finite group , is nilpotent and normal, and every normal nilpotent subgroup of is contained in . (The Fitting subgroup is nilpotent and is the largest normal nilpotent subgroup of a finite group).
Let , so that (def-natural-numbers). The symmetric group on letters is the group of all bijections of under composition (def-symmetric-group), with the composition convention. (The finite symmetric group , one-line notation, and cycle notation).
Verification
The subgroup is the unique Sylow -subgroup, so . The three order- subgroups are conjugate, so no nontrivial -subgroup is normal and . Therefore .
The maximal subgroups are and the three order- subgroups, whose intersection is ; hence . The quotient identity reduces to and is therefore satisfied. This proves the stated claim.
Depends on
- The Fitting subgroup $F(G)=\prod_p O_p(G)$ of a finite group
- The Frattini subgroup $\Phi(G)$ as the intersection of the maximal subgroups of a finite group
- The Fitting subgroup is nilpotent and is the largest normal nilpotent subgroup of a finite group
- The finite symmetric group $S_n$, one-line notation, and cycle notation
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 52 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.