Subgroup factorization from coset transitivity (source code)

= Subgroup factorization from coset transitivity
{title2=$G=HK\iff K\text{ is transitive on }H\backslash G$}

In the right multiplication action, the orbit of the coset $H$ under $K$ is $\{Hk:k\in K\}$. It is the whole right coset space exactly when every $g$ has form $hk$, proving the displayed criterion. The factorization need not be unique; for finite groups $|HK|=|H||K|/|H\cap K|$.