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.
If is finite then ; for finite this equals
Statement
Let . If is finite, then the quotient group is finite and
In particular, if is finite, then
Facts & Assumptions
Given: A group and a normal subgroup .
The index is the finite cardinality of the left-coset set when that set is finite (The coset set and the index of a subgroup).
If is finite and , then (Lagrange's theorem: for every subgroup of a finite group ).
The order of a finite group is the cardinality of its underlying set (The order of a finite group and the order of an element, with when no positive power of is the identity).
The quotient group has the left cosets of as its underlying set (For , the cosets form a group with identity and inverse ).
Proof
If is finite, then by [F1] the coset set underlying is finite with cardinality ; hence [F2] and [L2] give .
If is finite, then [L1] gives . Since contains the identity, , and step 1.1 yields .
The two asserted formulas follow.
Depends on
- For $N\mathrel{\trianglelefteq}G$, the cosets form a group with identity $N$ and inverse $(gN)^{-1}=g^{-1}N$
- The coset set $G/H$ and the index $[G:H]$ of a subgroup
- Lagrange's theorem: $|G|=[G:H]|H|$ for every subgroup $H$ of a finite group $G$
- The order $|G|$ of a finite group and the order $\operatorname{ord}(g)$ of an element, with $\operatorname{ord}(g) = \infty$ when no positive power of $g$ is the identity
Used by
- Converse of Lagrange for finite abelian groups: every divisor occurs as a subgroup order Corollary
- Every group of order p², for prime p, is abelian Corollary
- The order of a finite group is the product of the orders of its composition factors Corollary
- 1→⟨ i⟩→ Q₈→ Q₈/⟨ i⟩→1 does not split, with nonabelian middle group Counterexample
- A₄ has a normal Klein four subgroup and four conjugacy classes Example
- The three-cycle subgroup of Sym({1,2,3}) is normal and its quotient has two elements Example
- A nontrivial finite abelian p-group with a unique subgroup of order p is cyclic Lemma
- A normal Hall subgroup presents the ambient group as an extension of coprime orders Lemma
- If p<q are primes and |G|=pq, then G has a normal subgroup of order q Lemma
- The successive quotients pⁱG/pⁱ⁺¹G recover the cyclic summand multiplicities of a finite abelian p-group Lemma
- A maximal-order cyclic subgroup splits off a finite abelian p-group Theorem
- A p-primary component has the full p-power order and is the unique subgroup of that order Theorem
- Cauchy's theorem for finite abelian groups Theorem
- Every finite p-group is nilpotent Theorem
- Every group of order 105 has normal Sylow 5- and 7-subgroups and is not simple Theorem
- Every group of order 30 has normal Sylow 3- and 5-subgroups and is not simple Theorem
Dependency tree · two levels
24 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
- T. W. Judson, Abstract Algebra: Theory and Applications, Factor Groups and Normal Subgroups (standard reference, not scraped)