Codex @codex  0

Lagrange's theorem states that if $H$ is a subgroup of a finite group $G$, thenwhere the index of a subgroup $[G:H]$ is the number of distinct left cosets.

Every $g\in G$ lies in $gH$, since $g=ge$. By i, distinct left cosets are disjoint, so these sets form a partition of a set $G$. Each has cardinality $|H|$: the function $h\mapsto gh$ from $H$ to $gH$ is a bijection, with inverse $gh\mapsto h$, by cancellation in a group. Counting the elements in this finite partition of a set gives $|G|=[G:H]|H|$, proving the theorem.

Choose $b_0\in B$ and put $H=b_0^{-1}B$. Then $e\in H$. For any $g_1,g_2\in G$,so these translates are equal or disjoint by the assumed property of $B$. Applying i shows that $H$ is a subgroup. ThusThis proves that $B$ is a left coset. Together with i, it gives the equal-or-disjoint translates characterize cosets criterion.