Exact factorization of a group ($G=H_1{H}_2,H_1\cap H_2=\{e\}$)

Two subgroups give an exact factorization of a group when every element has a unique expression $h_1{h}_2$ with $h_i\in H_i$. Existence and trivial intersection are equivalent to this uniqueness: if $h_1{h}_2=k_1{k}_2$, then $k_1^{-1}{h}_1=k_2{h}_2^{-1}\in H_1\cap H_2$, so both sides are the identity. Conversely, an element $a$ in the intersection gives the two factorizations $a\cdot e=e\cdot a$, forcing $a=e$. For finite groups the multiplication map $H_1\times H_2\to G$ is therefore a bijection and $|G|=|H_1||H_2|$. It need not be a group homomorphism: an exact factorization is not automatically a direct product of groups. If $H_1$ is normal, it gives an internal semidirect product.