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.
Lagrange's theorem: for every subgroup of a finite group
Statement
Let be a finite group and . Then
Consequently, under the canonical embedding , divides .
Facts & Assumptions
Given: A finite group and a subgroup .
The distinct left cosets of partition (The left cosets of a subgroup partition the group).
The subgroup, every coset, and are finite; every coset has cardinality and (In a finite group, the subgroup, every coset and the set of cosets are finite, Every left or right coset of is equinumerous with , The coset set and the index of a subgroup).
For a finite partition , one has ; if every summand has the same value , then (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, The sum over a finite index set, and its product form).
The order of a finite group is the unique natural equinumerous with its underlying set, hence agrees with finite cardinality (The order of a finite group and the order of an element, with when no positive power of is the identity, The cardinality of a finite set).
The embedding preserves multiplication, and in means for some integer (The naturals embed in the integers, Divisibility in : when for some integer ).
Proof
Apply the finite partition sum to the coset partition: .
Every summand equals , and there are summands, so the constant-sum clause gives .
Applying gives , so .
Depends on
- In a finite group, the subgroup, every coset and the set of cosets are finite
- The left cosets of a subgroup partition the group
- Every left or right coset of $H$ is equinumerous with $H$
- The coset set $G/H$ and the index $[G:H]$ of a subgroup
- 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
- The cardinality $\lvert A\rvert$ of a finite set
- The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$, and a sum over a finite index set splits along a partition
- The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form
- Divisibility in $\mathbb{Z}$: $d \mid a$ when $a = dq$ for some integer $q$
- The naturals embed in the integers
Used by
- A noncentral element of an extraspecial p-group has centraliser of index p Corollary
- An extraspecial p-group has order p¹⁺²ⁿ for some n≥1 Corollary
- An extraspecial p-group is the product of two maximal abelian subgroups meeting in its centre Corollary
- Every subgroup of index p in a finite p-group is normal Corollary
- For a finite group, uniquely divisible coefficients have trivial first cohomology Corollary
- For an odd prime p, ℚ(ζₚ) has exactly one intermediate field of degree two over ℚ Corollary
- For K≤ H≤ G with G finite, [G:K]=[G:H][H:K] Corollary
- For n≥5, the only proper nontrivial normal subgroup of Sₙ is Aₙ Corollary
- If [G:N] is finite then |G/N|=[G:N]; for finite G this equals |G|/|N| Corollary
- Orbit-stabiliser cardinality: |G· x|=[G:Gₓ] whenever either side is finite, and |G|=|Gₓ| |G· x| for finite G Corollary
- The class equation of Sₙ is n!=∑_∑ k cₖ=n n!/∏ₖ k^cₖcₖ! Corollary
- The order of a finite group is the product of the orders of its composition factors Corollary
- The order of every element of a finite group divides the order of the group Corollary
- There are exactly two isomorphism classes of groups of order 105 Corollary
- 1→⟨ i⟩→ Q₈→ Q₈/⟨ i⟩→1 does not split, with nonabelian middle group Counterexample
- The product set HK of two subgroups need not be a subgroup Counterexample
- The subgroup ⟨(1 2 3),(1 2)(3 4)⟩≤ S₄ has order 12 but no subgroup of order 6, so Cauchy's theorem does not extend to composite divisors Counterexample
- The p-core Oₚ(G) as the largest normal p-subgroup Definition
- [G:G]=1 and, for finite G, [G:{e}]=|G| Example
- A₄ has no subgroup of order 6 Example
- Sylow p-subgroups of Aut((ℤ/p)²): nₚ=p+1 Example
- The Heisenberg group of order 27 has exponent 3 and thirteen subgroups of order 3 Example
- The modular group of order 27 has exponent 9 and exactly three cyclic subgroups of order 9 Example
- The subgroup orders in Sym({1,2,3}) are 1,2,3 and 6 Example
- The three maximal abelian subgroups of Dih(C₄) have order four, as the general bound predicts Example
- False statement: every divisor of the order of a finite group occurs as a subgroup order False statement
- FALSE: every finite abelian group is Gal(ℚ(μₙ)/ℚ) for some n False statement
- A finite cyclic group has exactly one subgroup of each order dividing its own Lemma
- A finite product of normal p-subgroups is a normal p-subgroup Lemma
- A normal Hall subgroup presents the ambient group as an extension of coprime orders Lemma
- A product formula for the number of square roots of the identity in a central product of extraspecial 2-groups Lemma
- A subgroup of the central quotient and its orthogonal complement have orders multiplying to the order of the quotient Lemma
- Distinct normal Sylow subgroups centralize one another Lemma
- Every subgroup of a finite p-group has order a power of p Lemma
- For primes p<q, nontrivial actions of Cₚ on C_q exist exactly when p∣(q-1) and are unique up to automorphisms Lemma
- If p<q are primes and |G|=pq, then G has a normal subgroup of order q Lemma
- Q₈∘ Q₈ congDih(C₄)circDih(C₄) Lemma
- The transitive subgroups of S₄ and their action on the three pairings Lemma
- Two elements of an extraspecial p-group with nontrivial commutator generate an extraspecial subgroup of order p³ Lemma
- Dih(C₄) and Q₈ are extraspecial of order 8, with six and two solutions of x²=1 respectively Proposition
…and 35 more results.
Dependency tree · two levels
49 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
- UCL lecture notes, Cosets and Lagrange's theorem (standard reference, not scraped)
- Thomas W. Judson, Abstract Algebra: Theory and Applications, §6.2: Lagrange's Theorem (standard reference, not scraped)