ThmDex – An index of mathematical definitions, results, and conjectures.
Result R468 on D1393: Subgroup index
Lagrange's theorem
Formulation 0
Let $G$ be a D1082: Finite group.
Let $H$ be a D496: Subgroup of $G$ such that
(i) $G / H$ is the D1396: Set of left cosets in $G$ modulo $H$
Then \begin{equation} |G / H| = \frac{|G|}{|H|} \end{equation}
Proofs
Proof 0
Let $G$ be a D1082: Finite group.
Let $H$ be a D496: Subgroup of $G$ such that
(i) $G / H$ is the D1396: Set of left cosets in $G$ modulo $H$
In the following, we apply the two important facts
(i) R643: Order of left coset modulo subgroup equals order of subgroup
(ii) R724: Set of left cosets partitions group

Since $G / H$ partitions $G$ it is, particularly, a set cover for $G$. That is, $G = \bigcup G / H$. Thus, using the fact that the order of each element of $G / H$ coincides with the order of $H$, we have \begin{equation} |G| = \left| \bigcup G / H \right| = \sum_{C \in G / H} |C| = \sum_{C \in G / H} |H| = |G / H| |H| \end{equation} Result R852: Group is not empty guarantees that $|H| \geq 1$. Thus, dividing each side by the nonzero integer $|H|$ then yields $|G / H| = |G| / |H|$. $\square$