---
tag: 3C53TD
kind: statement
role: theorem
name: Lagrange's theorem
msc: [20D60]
about: [G5S1M9, 0X1JXT47GA, 03DEH43F4H, 0B85S2V2DR]
uses: [G5S1M9]
formal:
  - system: lean4
    library: mathlib
    decl: Subgroup.card_subgroup_dvd_card
    match: stronger
    adapter: Math2.Match.lagrange
sources:
  - book: isbn:9780471433347
    locator: Section 3.2, Theorem 8
inventory: [ADBP6KTNFC]
---

## Statement

Let $G$ be a finite [[group|G5S1M9]] and let $H$ be a subgroup of $G$.
Then the order of $H$ divides the order of $G$.

## Remarks

The quotient $|G| / |H|$ is the number of left cosets of $H$ in $G$.

## Explanations

### L1 agent

The left cosets of a subgroup cut the group into pieces of the same size.
Each piece has as many elements as the subgroup.
Thus the size of the group is a whole number of copies of the size of the subgroup.
For example, a group with $12$ elements can have subgroups of order $1, 2, 3, 4, 6$ or $12$, and of no other order.

### L2 agent

Lagrange's theorem gives a strong limit on the subgroups of a finite group. The order of each subgroup is a divisor of the order of the group.

The idea of the proof is to count cosets:

1. The left cosets $aH$ of $H$ partition $G$.
2. Each left coset has exactly $|H|$ elements, because $h \mapsto ah$ is a bijection from $H$ to $aH$.
3. If there are $k$ cosets, then $|G| = k\,|H|$.

The number $k$ is the index $[G : H]$. Thus $|G| = [G : H] \cdot |H|$.

A worked example with $G = \mathbb{Z}/12\mathbb{Z}$ and $H = \{0, 4, 8\}$:

1. $H$ is a subgroup of order $3$.
2. The cosets are $H$, $1 + H = \{1, 5, 9\}$, $2 + H = \{2, 6, 10\}$ and $3 + H = \{3, 7, 11\}$.
3. There are $4$ cosets of $3$ elements each, and $4 \cdot 3 = 12$.

Two standard consequences are that the order of each element divides $|G|$, and that a group of prime order is cyclic.

A common error is to believe the converse. A divisor $d$ of $|G|$ need not be the order of a subgroup. The alternating group $A_4$ has order $12$, but it has no subgroup of order $6$. The converse is true for some classes of groups, for example for cyclic groups and for groups of prime power order.

The theorem needs $G$ to be finite. For an infinite group the index can still be finite, as for $2\mathbb{Z}$ in $\mathbb{Z}$, but the orders are not numbers.