Si H est un sous-groupe de G fini, alors |H| divise |G|.
On considère la relation d'équivalence : x ~ y ⟺ x⁻¹y ∈ H. Les classes d'équivalence sont les classes à gauche gH = gh : h ∈ H. Toutes les classes ont le même cardinal |H| (bijection g· : H → gH). Les classes partitionnent G, donc |G| = [G:H] · |H|.