proposition: Lemma Frobenius_reciprocity phi psi : '[phi, 'Res[H] psi] = '['Ind[G] phi, psi].
proof: Proof. have [sHG | not_sHG] := boolP (H \subset G); last first. rewrite cfResEout // cfIndEout // cfdotZr cfdotZl mulrAC; congr (_ * _). rewrite (cfdotEl _ (cfuni_on _ _)) mulVKf ?neq0CG // big_set1. by rewrite cfuniE ?normal1 ?set11 ?mul1r. transitivity (#|H|%:R^-1 * \sum_(x in G) phi x * (psi x)^* ). rewrite (big_setID H) /= (setIidPr sHG) addrC big1 ?add0r; last first. by move=> x /setDP[_ /cfun0->]; rewrite mul0r. by congr (_ * _); apply: eq_bigr => x Hx; rewrite cfResE. set h' := _^-1; apply: canRL (mulKf (neq0CG G)) _. transitivity (h' * \sum_(y in G) \sum_(x in G) phi (x ^ y) * (psi (x ^ y))^* ). rewrite mulrCA mulr_natl -sumr_const; congr (_ * _); apply: eq_bigr => y Gy. by rewrite (reindex_acts 'J _ Gy) ?astabsJ ?normG. rewrite exchange_big mulr_sumr; apply: eq_bigr => x _; rewrite cfIndE //=. by rewrite -mulrA mulr_suml; congr (_ * _); apply: eq_bigr => y /(cfunJ psi)->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)