Desires for normalizers and orbits (now 5.5/5.6)

[bidundas]

How I state later stuff depends on the implementation - I'm not asking for things to be implemented now, I just want to know how one intends to so that I can comply.

1 I need to refer to the normalizer. Ideally in a form reflecting that (classically speaking) if H is a subgroup of G, then the fixed points [G/H]^H is a group whose preimage in G is called N_G(H) (and of course that N_G(H)->[G/H]^H is a group homomorphism).

2. I also refer to Burnside's lemma, but the only thing I'll actually need is that if G is finite and X is a finite G-set, then X consists of the G-fixed points and the nontrivial orbits and that the cardinality of the latter divides the order of G.

[UlrikBuchholtz]

Re 2: Commit 0377cd8 adds a proof of Burnside in the desired form.

Re 1: Noted, and thy wish shall be granted.

[UlrikBuchholtz]

Re 2 again, it's not quite in the desired form, but I'll add that as a corollary later.