Exact factorization of a group (source code)

= Exact factorization of a group
{title2=$G=H_1H_2,\quad H_1\cap H_2=\{e\}$}

Two <subgroups> give an exact factorization of a <group> when every element has a unique expression $h_1h_2$ with $h_i\in H_i$. Existence and trivial intersection are equivalent to this uniqueness: if $h_1h_2=k_1k_2$, then $k_1^{-1}h_1=k_2h_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>.