Theorem·T13
Lagrange's theorem
The size of a subgroup divides the size of the group.
Let
be a group with
finite, and
a subgroup. Then
more precisely,
where
is the number of distinct left cosets of
(the index of
in
). Divisibility from D030, cardinality from D035, equinumerosity from D033.
In words
Let G with operation ⋆ be a finite group and H a subgroup of G. Then the size of H divides the size of G: more precisely, the size of G is k times the size of H, where k is the number of distinct left cosets of H, the index of H in G.
Never needed: F10 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1Let be the coset relation . By L29 it is an equivalence relation on whose classes are the left cosets: .
- 2
- 3The quotient is finite: the map with domain sending to is a function (a set by Separation inside ; each has exactly one class), and it is surjective: every member of is for some (D022). Since is finite, L25 makes finite; let , so (D035).
- 4
- 5
- 6Divisibility: by commutativity, so with witness (D030): the order of divides the order of .
∎
Remarks
Joseph-Louis Lagrange stated a version in 1770 for permutations arising from polynomials, decades before abstract groups existed; the modern statement is the first structural fact every student learns about finite groups. The proof is pure counting: cosets tile the group (T04), each tile is a copy of
(L30), so the group is
tiles of
elements (L27). The number
is the index
. Standard consequences (not yet formalized here, as they need cyclic subgroups): the order of every element divides
, groups of prime order have no subgroups beyond the trivial two, and Fermat's little theorem. The converse of Lagrange fails: the alternating group
has
elements but no subgroup of size
.