Solution (source code)

= Solution

For a <group action>, the <orbit of a group action> of $x$ is $Gx=\{gx:g\in G\}$, and its <stabilizer subgroup> is $G_x=\{g:gx=x\}$. The <orbit-stabilizer theorem> gives $|Gx||G_x|=|G|$: the map $gG_x\mapsto gx$ is a well-defined <bijection> from stabilizer <cosets> to the orbit.

Within one orbit, the <stabilizer subgroups> are conjugate, since $G_{hx}=hG_xh^{-1}$. Their sizes are therefore equal. Summing stabilizer sizes over a single orbit gives $|Gx||G_x|=|G|$, and summing over all $n$ orbits yields
$$
\boxed{\sum_{x\in X}|\operatorname{Stab}(x)|=n|G|.}
$$
Now count the pairs $(g,x)$ fixed by the action in two ways. Holding $x$ fixed gives $|G_x|$ choices of $g$, whereas holding $g$ fixed gives $|\operatorname{Fix}(g)|$ choices of $x$. Thus
$$
|S|=\sum_{x\in X}|G_x|=\sum_{g\in G}|\operatorname{Fix}(g)|.
$$
Combining the two identities proves <Burnside lemma>:
$$
\boxed{n=\frac1{|G|}\sum_{g\in G}|\operatorname{Fix}(g)|.}
$$
The finiteness hypotheses justify these cardinality sums. If $X$ is empty, every sum and the orbit count are zero, so the formula still applies.