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.
Maximal subgroups of finite nilpotent groups are normal of prime index
Statement
Every maximal proper subgroup of a finite nilpotent group is normal and has prime index. See Maximal proper subgroups.
Facts & Assumptions
Given: The hypotheses and objects in the Statement.
A subgroup is maximal proper when there is no subgroup with . Equivalently, every subgroup containing is either or . The word maximal refers to inclusion among proper subgroups, not to cardinality. (Maximal proper subgroups).
Every proper subgroup of a finite nilpotent group is properly contained in its normalizer. (Every proper subgroup of a finite nilpotent group is properly contained in its normalizer).
Let be a finite group and let be prime. If , then contains an element of order . (Cauchy's theorem: if a prime divides , then has an element of order ).
Every subgroup and every quotient of a nilpotent group is nilpotent. Every finite direct product of nilpotent groups is nilpotent; the class of a subgroup or quotient is at most the class of the original group, and the class of a nonempty finite product is at most the maximum of the factor classes. The empty product is the trivial group of class zero. (Subgroups, quotients, and finite direct products of nilpotent groups are nilpotent).
Proof
The normalizer condition and maximality force , hence .
The quotient has no nontrivial proper subgroup; Cauchy's theorem then forces its nontrivial order to be prime.
A maximal subgroup is proper by definition, so and the quotient of step 2.1 is nontrivial; its order is therefore a genuine prime rather than , and step 1.1 has already made normal. This proves the stated claim.
Depends on
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 88 results over 19 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.
Sources
- Keith Conrad, Consequences of the Sylow Theorems, Sections 1-5 (standard reference, not scraped)