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.
False statement: finite nilpotent groups and finite solvable groups are the same
Statement
False claim: finite nilpotent groups and finite solvable groups are the same. See Nilpotent groups, and in particular finite -groups, are solvable.
Facts & Assumptions
Given: The hypotheses and objects in the false claim.
Every nilpotent group is solvable. Consequently every finite -group is solvable. (Nilpotent groups, and in particular finite -groups, are solvable).
The derived series of a group is defined recursively by Each term is characteristic, hence normal, in the preceding term by thm-derived-subgroup-is-characteristic-and-abelianization-is-universal. (The derived series, solvable groups, and derived length).
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).
For a finite group , the following are equivalent: is nilpotent; every Sylow subgroup is normal; is the internal direct product of its Sylow subgroups; and every maximal subgroup of is normal. (Sylow and maximal-subgroup characterizations of finite nilpotence).
Refutation
One inclusion does hold: [L1] states that every nilpotent group is solvable, so every finite nilpotent group is solvable and only the converse can fail. Refuting the claim therefore requires a finite solvable group that is not nilpotent.
For the converse, take of [L3] and compute its derived series of [L2]: and , so is solvable. Its three Sylow -subgroups are the subgroups generated by the transpositions, which are not normal, so the maximal-subgroup and Sylow clauses of [L4] deny that is nilpotent. A finite solvable group that is not nilpotent refutes the claim. This proves the stated claim.
Depends on
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: 78 results over 15 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)