Solution (source code)

= Solution

For a finite <group> $G$, subgroups $H,K$, and a complex <group representation> $V$ of $H$, the <Mackey restriction formula> is
$$
\boxed{\operatorname{Res}^{G}_{K}\operatorname{Ind}^{G}_{H}V\cong\bigoplus_{g\in K\backslash G/H}\operatorname{Ind}^{K}_{K\cap gHg^{-1}}\operatorname{Res}^{gHg^{-1}}_{K\cap gHg^{-1}}({}^{g}V).}
$$
Choose one representative $g$ of each <double coset> $KgH$. The <conjugate subgroup representation> ${}^{g}V$ is a representation of $gHg^{-1}$ on the same vector space, with $(ghg^{-1})v=hv$. <Restriction of a representation> keeps the vector space and restricts the acting subgroup. <induced representation> is $\mathbb CG\otimes_{\mathbb CH}V$, and analogously for each subgroup of $K$. The displayed isomorphism is an isomorphism of $K$-representations. These definitions specify every summand and its subgroup.