points of X fixed by g ∈ G, whereas Gx = {g ∈ G | g.x = x} is the stabilizer subgroup of G that fixes the point x ∈ X.) The orbit-stabilizer theorem says that there is a natural bijection for each x ∈ X between the orbit of x, G·x = {g·x | g ∈ G} ⊆ X, and the set of left cosets G/Gx of its stabilizer subgroup Gx. With Lagrange's theorem this implies Our sum over the set X may therefore be rewritten as Finally, notice that X is the disjoint union of all its orbits in X/G, which means the sum over X may be broken up into separate sums over each individual orbit. Putting everything together gives the desired result: This proof is essentially also the proof of the class equation formula, simply by taking the action of G on itself (X = G) to be by conjugation, g.x = gxg−1, in which case Gx instantiates to the centralizer of x in G. Ease of application Unlike some formulas, applying Burnside's Lemma is usually not as simple as plugging in a few readily available values. In general, for a set X of n objects and a group G of m actions, there are nm cases to consider as to whether a particular action leaves a particular object unchanged. The null action is often easy to account for, for example when X is the set of bit vectors of length k, the size of X is 2k. But there is no known simple formula for the 92 solutions unaffected by the null action in the 8-queens puzzle. In some cases, clever insight can account for the effects of certain actions. For example when X is the set of bit vectors of length k, and k is prime, rotations other than the null rotation will leave only two bit vectors unchanged, those with all zeros or all ones. Enumeration vs. generation Burnside's Lemma counts distinct objects, but it doesn't generate them. In general, combinatorial generation with isomorph rejection considers the same |G| actions, g, on the same |X| objects, x. But instead of checking that g.x=x, it checks that g.x has not already been generated. One way to accomplish this is by checking that g.x is not lexicographically less than x, using the lexicographically least member of each equivalence class as the class representative. Counting the