theorem Hex.PermGroup.Group.wreathProduct_order {n m : Nat} (G : Group n) (H : Group m) (hn : 0 < n) : (G.wreathProduct H).order = G.order ^ m * H.order

The faithful imprimitive action has one independent base factor per declared block, whether or not the top action is transitive.

theorem Hex.PermGroup.Group.wreath_zero {n : Nat} (G : Group n) (H : Group 0) : (G.wreathProduct H).order = 1

No blocks give the trivial action, including when the base group itself is nontrivial.