Alphabeta MathHow 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.
If is characteristic in and is normal in , then is normal in
Statement
If is characteristic in and , then .
Facts & Assumptions
Given: Subgroups with characteristic in and normal in .
A characteristic subgroup is preserved by every automorphism of its ambient group (Characteristic subgroups).
A subgroup is normal exactly when conjugation by every ambient element preserves it (Normal subgroup: invariance under conjugation).
Conjugation by a fixed group element is an automorphism (Conjugation is an automorphism).
Proof
Fix . Normality of and [L2] show that conjugation by maps to itself; by [L3], its restriction is an automorphism of .
Since is characteristic in , [L1] gives . This holds for every , so by [L2].
Depends on
Used by
- A normal Sylow subgroup of a normal subgroup is normal in the whole group Corollary
- A nontrivial normal subgroup of a solvable group contains a nontrivial abelian subgroup normal in the whole group Lemma
- Minimal normal subgroups of finite groups are characteristically simple Lemma
- Nilpotence lifts over the Frattini subgroup of a finite group Theorem
- Schur-Zassenhaus existence theorem Theorem
- The Fitting subgroup is nilpotent and is the largest normal nilpotent subgroup of a finite group Theorem
- The generalized Fitting subgroup contains its centralizer Theorem
Dependency tree · two levels
7 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. S. Milne, Group Theory (standard reference, not scraped)