Lagrange's Theorem states that if $G$ is a finite Group and $H$ a subgroup, then the order $|H|$ of $H$ divides the order $|G|$ of $G$. It generalises to infinite groups: the statement then becomes that the left cosets form a [set_partition partition], and for any pair of cosets, there is a bijection between them.

Proof

In full generality, the cosets form a partition and are all in bijection.

To specialise this to the finite case, we have divided the $|G|$ elements of $G$ into buckets of size $|H|$ (namely, the cosets), so $|G|/|H|$ must in particular be an integer.