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 quotient group and coset product
Definition
Let be a group and let be a normal subgroup (Normal subgroup: invariance under conjugation). The quotient group, or factor group, has the left cosets
as its elements (Left and right cosets and of a subgroup, The coset set and the index of a subgroup), with product
Independence of the chosen representatives is proved in Coset multiplication is well defined if and only if is normal ↗, and the group axioms are proved in For , the cosets form a group with identity and inverse ↗.
Depends on
Used by
- Converse of Lagrange for finite abelian groups: every divisor occurs as a subgroup order Corollary
- Group presentation by generators and relations Definition
- Quotient module M/N with scalar multiplication on additive cosets Definition
- The abelianisation Gᵃᵇ:=G/[G,G] and its canonical map Definition
- The quotient ring R/I with (r+I)(s+I)=rs+I Definition
- A nontrivial finite abelian p-group with a unique subgroup of order p is cyclic Lemma
- If G/Z(G) is cyclic, then G is abelian Lemma
- If K is normal in G, N is normal in G and K⊆ N, then N/K is normal in G/K Lemma
- The successive quotients pⁱG/pⁱ⁺¹G recover the cyclic summand multiplicities of a finite abelian p-group Lemma
- In ⟨ X∣ R⟩, the words u and v represent the same element if and only if u⁻¹v∈⟨⟨ R⟩⟩ Proposition
- A group pushout is the quotient of a free product by the amalgamating relations Theorem
- A homomorphism that kills a normal subgroup factors uniquely through the quotient group Theorem
- A maximal-order cyclic subgroup splits off a finite abelian p-group Theorem
- Cauchy's theorem for finite abelian groups Theorem
- Correspondence theorem: subgroups of G/N correspond to subgroups of G containing N, with normality preserved Theorem
- Coset multiplication (gH)(hH)=ghH is well defined if and only if H is normal Theorem
- For N is normal in G, the cosets form a group with identity N and inverse (gN)⁻¹=g⁻¹N Theorem
- If [G:H]=n<∞, then Core_G(H) is normal in G, [G:Core_G(H)]∣ n!, and only finitely many subgroups contain H Theorem
- Multiplication of additive cosets is well defined if and only if the additive subgroup is a two-sided ideal Theorem
- Second isomorphism theorem for groups: H/(H∩ N)≅ HN/N Theorem
- Third isomorphism theorem for groups: (G/K)/(N/K)≅ G/N Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 24 results over 11 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
- T. W. Judson, Abstract Algebra: Theory and Applications, Factor Groups and Normal Subgroups (standard reference, not scraped)