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 and , then is a subgroup and
Statement
If and , then is a subgroup and .
Here .
Facts & Assumptions
Given: A subgroup and a normal subgroup .
A nonempty subset closed under is a subgroup (One-step subgroup test: a nonempty is a subgroup iff for all ; the identity and the inverses of are then those of ).
Normality means for every (Normal subgroup: invariance under conjugation).
A subgroup is normal if its conjugates by ambient elements lie in it (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).
Proof
The identity lies in ; for , put , so .
Thus [L1] gives ; moreover for and , both and , so it lies in .
The conjugation closure in step 2.1 gives .
Depends on
- One-step subgroup test: a nonempty $H \subseteq G$ is a subgroup iff $gh^{-1} \in H$ for all $g, h \in H$; the identity and the inverses of $H$ are then those of $G$
- Normal subgroup: invariance under conjugation
- Equivalent characterisations of a normal subgroup by conjugates and left and right cosets
- In a group $e^{-1} = e$, $(g^{-1})^{-1} = g$ and $(gh)^{-1} = h^{-1}g^{-1}$, the order of the last product being essential
Used by
- There are exactly two isomorphism classes of groups of order 105 Corollary
- The p-core Oₚ(G) as the largest normal p-subgroup Definition
- A finite product of normal p-subgroups is a normal p-subgroup Lemma
- Classification of groups of order pq for primes p<q Theorem
- Every group of order 105 has normal Sylow 5- and 7-subgroups and is not simple Theorem
- Frattini argument: if N is normal in G and P is Sylow in N, then G=N N_G(P) Theorem
- Internal direct products are external direct products, equivalently every element has a unique factorisation Theorem
- Second isomorphism theorem for groups: H/(H∩ N)≅ HN/N Theorem
- Φ(P)=P'Pᵖ for a finite p-group Theorem
Dependency tree · two levels
11 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
- Judson, Abstract Algebra: Theory and Applications, Isomorphism Theorems (standard reference, not scraped)