move odd_order to its own repository

1 files changed, 0 insertions, 830 deletions

diff --git a/mathcomp/odd_order/PFsection2.v b/mathcomp/odd_order/PFsection2.v
deleted file mode 100644
index c982642..0000000
--- a/mathcomp/odd_order/PFsection2.v
+++ /dev/null
@@ -1,830 +0,0 @@
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
-(* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrbool ssrfun eqtype ssrnat seq path div choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg poly finset center.
-From mathcomp
-Require Import fingroup morphism perm automorphism quotient action zmodp.
-From mathcomp
-Require Import gfunctor gproduct cyclic pgroup frobenius ssrnum.
-From mathcomp
-Require Import matrix mxalgebra mxrepresentation vector algC classfun character.
-From mathcomp
-Require Import inertia vcharacter PFsection1.
-
-(******************************************************************************)
-(* This file covers Peterfalvi, Section 2: the Dade isometry                  *)
-(* Defined here:                                                              *)
-(*   Dade_hypothesis G L A <-> G, L, and A satisfy the hypotheses under which *)
-(*                               which the Dade isometry relative to G, L and *)
-(*                               A is well-defined.                           *)
-(* For ddA : Dade_hypothesis G L A, we also define                            *)
-(*              Dade ddA == the Dade isometry relative to G, L and A.         *)
-(* Dade_signalizer ddA a == the normal complement to 'C_L[a] in 'C_G[a] for   *)
-(*                          a in A (this is usually denoted by H a).          *)
-(*   Dade_support1 ddA a == the set of elements identified with a by the Dade *)
-(*                         isometry.                                          *)
-(*      Dade_support ddA == the natural support of the Dade isometry.         *)
-(* The following are used locally in expansion of the Dade isometry as a sum  *)
-(* of induced characters:                                                     *)
-(*         Dade_transversal ddA == a transversal of the L-conjugacy classes   *)
-(*                                 of non empty subsets of A.                 *)
-(*    Dade_set_signalizer ddA B == the generalization of H to B \subset A,    *)
-(*                                 denoted 'H(B) below.                       *)
-(*    Dade_set_normalizer ddA B == the generalization of 'C_G[a] to B.        *)
-(*                                 denoted 'M(B) = 'H(B) ><| 'N_L(B) below.   *)
-(*    Dade_cfun_restriction ddA B aa == the composition of aa \in 'CF(L, A)   *)
-(*                                 with the projection of 'M(B) onto 'N_L(B), *)
-(*                                 parallel to 'H(B).                         *)
-(* In addition, if sA1A : A1 \subset A and nA1L : L \subset 'N(A1), we have   *)
-(*  restr_Dade_hyp ddA sA1A nA1L : Dade_hypothesis G L A1 H                   *)
-(*      restr_Dade ddA sA1A nA1L == the restriction of the Dade isometry to   *)
-(*                                  'CF(L, A1).                               *)
-(******************************************************************************)
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-
-Import GroupScope GRing.Theory Num.Theory.
-Local Open Scope ring_scope.
-
-Reserved Notation "alpha ^\tau" (at level 2, format "alpha ^\tau").
-
-Section Two.
-
-Variable gT : finGroupType.
-
-(* This is Peterfalvi (2.1). *)
-Lemma partition_cent_rcoset (H : {group gT}) g (C := 'C_H[g]) (Cg := C :* g) :
-    g \in 'N(H) -> coprime #|H| #[g] ->
-  partition (Cg :^: H) (H :* g) /\ #|Cg :^: H| = #|H : C|.
-Proof.
-move=> nHg coHg; pose pi := \pi(#[g]).
-have notCg0: Cg != set0 by apply/set0Pn; exists g; apply: rcoset_refl.
-have id_pi: {in Cg, forall u, u.`_ pi = g}.
-  move=> _ /rcosetP[u /setIP[Hu cgu] ->]; rewrite consttM; last exact/cent1P.
-  rewrite (constt_p_elt (pgroup_pi _)) (constt1P _) ?mul1g //.
-  by rewrite (mem_p_elt _ Hu) // /pgroup -coprime_pi' // coprime_sym.
-have{id_pi} /and3P[_ tiCg /eqP defC]: normedTI Cg H C.
-  apply/normedTI_P; rewrite subsetI subsetIl normsM ?normG ?subsetIr //.
-  split=> // x Hx /pred0Pn[u /andP[/= Cu Cxu]]; rewrite !inE Hx /= conjg_set1.
-  by rewrite -{2}(id_pi _ Cu) -(conjgKV x u) consttJ id_pi -?mem_conjg.
-have{tiCg} partCg := partition_class_support notCg0 tiCg.
-have{defC} oCgH: #|Cg :^: H| = #|H : C| by rewrite -defC -astab1Js -card_orbit.
-split=> //; congr (partition _ _): (partCg); apply/eqP.
-rewrite eqEcard card_rcoset {1}class_supportEr; apply/andP; split.
-  apply/bigcupsP=> x Hx; rewrite conjsgE -rcosetM conjgCV rcosetM mulgA.
-  by rewrite mulSg ?mul_subG ?subsetIl // sub1set ?memJ_norm ?groupV.
-have oCg Cx: Cx \in Cg :^: H -> #|Cx| = #|C|.
-  by case/imsetP=> x _ ->; rewrite cardJg card_rcoset.
-by rewrite (card_uniform_partition oCg partCg) oCgH mulnC Lagrange ?subsetIl.
-Qed.
-
-Definition is_Dade_signalizer (G L A : {set gT}) (H : gT -> {group gT}) :=
-  {in A, forall a, H a ><| 'C_L[a] = 'C_G[a]}.
-
-(* This is Peterfalvi Definition (2.2). *)
-Definition Dade_hypothesis (G L A : {set gT}) :=
-  [/\ A <| L, L \subset G, 1%g \notin A,
-   (*a*) {in A &, forall x, {subset x ^: G <= x ^: L}}
- & (*b*) exists2 H, is_Dade_signalizer G L A H
- & (*c*) {in A &, forall a b, coprime #|H a| #|'C_L[b]| }].
-
-Variables (G L : {group gT}) (A : {set gT}).
-
-Let pi := [pred p | [exists a in A, p \in \pi('C_L[a])]].
-
-Let piCL a : a \in A -> pi.-group 'C_L[a].
-Proof.
-move=> Aa; apply: sub_pgroup (pgroup_pi _) => p cLa_p.
-by apply/exists_inP; exists a.
-Qed.
-
-Fact Dade_signalizer_key : unit. Proof. by []. Qed.
-Definition Dade_signalizer_def a := 'O_pi^'('C_G[a])%G.
-Definition Dade_signalizer of Dade_hypothesis G L A :=
-  locked_with Dade_signalizer_key Dade_signalizer_def.
-
-Hypothesis ddA : Dade_hypothesis G L A.
-Notation H := (Dade_signalizer ddA).
-Canonical Dade_signalizer_unlockable := [unlockable fun H].
-
-Let pi'H a : pi^'.-group (H a). Proof. by rewrite unlock pcore_pgroup. Qed.
-Let nsHC a : H a <| 'C_G[a]. Proof. by rewrite unlock pcore_normal. Qed.
-
-Lemma Dade_signalizer_sub a : H a \subset G.
-Proof. by have /andP[/subsetIP[]] := nsHC a. Qed.
-
-Lemma Dade_signalizer_cent a : H a \subset 'C[a].
-Proof. by have /andP[/subsetIP[]] := nsHC a. Qed.
-
-Let nsAL : A <| L. Proof. by have [->] := ddA. Qed.
-Let sAL : A \subset L. Proof. exact: normal_sub nsAL. Qed.
-Let nAL : L \subset 'N(A). Proof. exact: normal_norm nsAL. Qed.
-Let sLG : L \subset G. Proof. by have [_ ->] := ddA. Qed.
-Let notA1 : 1%g \notin A. Proof. by have [_ _ ->] := ddA. Qed.
-Let conjAG : {in A &, forall x, {subset x ^: G <= x ^: L}}.
-Proof. by have [_ _ _ ? _] := ddA. Qed.
-Let sHG := Dade_signalizer_sub.
-Let cHA := Dade_signalizer_cent.
-Let notHa0 a : H a :* a :!=: set0.
-Proof. by rewrite -cards_eq0 -lt0n card_rcoset cardG_gt0. Qed.
-
-Let HallCL a : a \in A -> pi.-Hall('C_G[a]) 'C_L[a].
-Proof.
-move=> Aa; have [_ _ _ _ [H1 /(_ a Aa)/sdprodP[_ defCa _ _] coH1L]] := ddA.
-have [|//] := coprime_mulGp_Hall defCa _ (piCL Aa).
-apply: sub_pgroup (pgroup_pi _) => p; apply: contraL => /exists_inP[b Ab].
-by apply: (@pnatPpi \pi(_)^'); rewrite -coprime_pi' ?cardG_gt0 ?coH1L.
-Qed.
-
-Lemma def_Dade_signalizer H1 : is_Dade_signalizer G L A H1 -> {in A, H =1 H1}.
-Proof.
-move=> defH1 a Aa; apply/val_inj; rewrite unlock /=; have defCa := defH1 a Aa.
-have /sdprod_context[nsH1Ca _ _ _ _] := defCa.
-by apply/normal_Hall_pcore=> //; apply/(sdprod_normal_pHallP _ (HallCL Aa)).
-Qed.
-
-Lemma Dade_sdprod : is_Dade_signalizer G L A H.
-Proof.
-move=> a Aa; have [_ _ _ _ [H1 defH1 _]] := ddA.
-by rewrite (def_Dade_signalizer defH1) ?defH1.
-Qed.
-Let defCA := Dade_sdprod.
-
-Lemma Dade_coprime : {in A &, forall a b, coprime #|H a| #|'C_L[b]| }.
-Proof. by move=> a b _ Ab; apply: p'nat_coprime (pi'H a) (piCL Ab). Qed.
-Let coHL := Dade_coprime.
-
-Definition Dade_support1 a := class_support (H a :* a) G.
-Local Notation dd1 := Dade_support1.
-
-Lemma mem_Dade_support1 a x : a \in A -> x \in H a -> (x * a)%g \in dd1 a.
-Proof. by move=> Aa Hx; rewrite -(conjg1 (x * a)) !mem_imset2 ?set11. Qed.
-
-(* This is Peterfalvi (2.3), except for the existence part, which is covered  *)
-(* below in the NormedTI section.                                             *)
-Lemma Dade_normedTI_P :
-  reflect (A != set0 /\ {in A, forall a, H a = 1%G}) (normedTI A G L).
-Proof.
-apply: (iffP idP) => [tiAG | [nzA trivH]].
-  split=> [|a Aa]; first by have [] := andP tiAG.
-  apply/trivGP; rewrite -(coprime_TIg (coHL Aa Aa)) subsetIidl subsetI cHA.
-  by rewrite (subset_trans (normal_sub (nsHC a))) ?(cent1_normedTI tiAG).
-apply/normedTI_memJ_P; split=> // a g Aa Gg.
-apply/idP/idP=> [Aag | Lg]; last by rewrite memJ_norm ?(subsetP nAL).
-have /imsetP[k Lk def_ag] := conjAG Aa Aag (mem_imset _ Gg).
-suffices: (g * k^-1)%g \in 'C_G[a].
-  by rewrite -Dade_sdprod ?trivH // sdprod1g inE groupMr ?groupV // => /andP[].
-rewrite !inE groupM ?groupV // ?(subsetP sLG) //=.
-by rewrite conjg_set1 conjgM def_ag conjgK.
-Qed.
-
-(* This is Peterfalvi (2.4)(a) (extended to all a thanks to our choice of H). *)
-Lemma DadeJ a x : x \in L -> H (a ^ x) :=: H a :^ x.
-Proof.
-by move/(subsetP sLG)=> Gx; rewrite unlock -pcoreJ conjIg -cent1J conjGid.
-Qed.
-
-Lemma Dade_support1_id a x : x \in L -> dd1 (a ^ x) = dd1 a.
-Proof.
-move=> Lx; rewrite {1}/dd1 DadeJ // -conjg_set1 -conjsMg.
-by rewrite class_supportGidl ?(subsetP sLG).
-Qed.
-
-Let piHA a u : a \in A -> u \in H a :* a -> u.`_pi = a.
-Proof.
-move=> Aa /rcosetP[{u}u Hu ->]; have pi'u: pi^'.-elt u by apply: mem_p_elt Hu.
-rewrite (consttM _ (cent1P (subsetP (cHA a) u Hu))).
-suffices pi_a: pi.-elt a by rewrite (constt1P pi'u) (constt_p_elt _) ?mul1g.
-by rewrite (mem_p_elt (piCL Aa)) // inE cent1id (subsetP sAL).
-Qed.
-
-(* This is Peterfalvi (2.4)(b). *)
-Lemma Dade_support1_TI : {in A &, forall a b,
-  ~~ [disjoint dd1 a & dd1 b] -> exists2 x, x \in L & b = a ^ x}.
-Proof.
-move=> a b Aa Ab /= /pred0Pn[_ /andP[/imset2P[x u /(piHA Aa) def_x Gu ->]]] /=.
-case/imset2P=> y v /(piHA Ab) def_y Gv /(canLR (conjgK v)) def_xuv.
-have def_b: a ^ (u * v^-1) = b by rewrite -def_x -consttJ conjgM def_xuv def_y.
-by apply/imsetP/conjAG; rewrite // -def_b mem_imset ?groupM ?groupV.
-Qed.
-
-(* This is an essential strengthening of Peterfalvi (2.4)(c). *)
-Lemma Dade_cover_TI : {in A, forall a, normedTI (H a :* a) G 'C_G[a]}.
-Proof.
-move=> a Aa; apply/normedTI_P; split=> // [|g Gg].
-  by rewrite subsetI subsetIl normsM ?subsetIr ?normal_norm ?nsHC.
-rewrite disjoint_sym => /pred0Pn[_ /andP[/imsetP[u Ha_u ->] Ha_ug]].
-by rewrite !inE Gg /= conjg_set1 -{1}(piHA Aa Ha_u) -consttJ (piHA Aa).
-Qed.
-
-(* This is Peterfalvi (2.4)(c). *)
-Lemma norm_Dade_cover : {in A, forall a, 'N_G(H a :* a) = 'C_G[a]}.
-Proof. by move=> a /Dade_cover_TI /and3P[_ _ /eqP]. Qed.
-
-Definition Dade_support := \bigcup_(a in A) dd1 a.
-Local Notation Atau := Dade_support.
-
-Lemma not_support_Dade_1 : 1%g \notin Atau.
-Proof.
-apply: contra notA1 => /bigcupP[a Aa /imset2P[u x Ha_u _ ux1]].
-suffices /set1P <-: a \in [1] by [].
-have [_ _ _ <-] := sdprodP (defCA Aa).
-rewrite 2!inE cent1id (subsetP sAL) // !andbT.
-by rewrite -groupV -(mul1g a^-1)%g -mem_rcoset -(conj1g x^-1) ux1 conjgK.
-Qed.
-
-Lemma Dade_support_sub : Atau \subset G.
-Proof.
-apply/bigcupsP=> a Aa; rewrite class_support_subG // mul_subG ?sHG //.
-by rewrite sub1set (subsetP sLG) ?(subsetP sAL).
-Qed.
-
-Lemma Dade_support_norm : G \subset 'N(Atau).
-Proof.
-by rewrite norms_bigcup //; apply/bigcapsP=> a _; apply: class_support_norm.
-Qed.
-
-Lemma Dade_support_normal : Atau <| G.
-Proof. by rewrite /normal Dade_support_sub Dade_support_norm. Qed.
-
-Lemma Dade_support_subD1 : Atau \subset G^#.
-Proof. by rewrite subsetD1 Dade_support_sub not_support_Dade_1. Qed.
-
-(* This is Peterfalvi Definition (2.5). *)
-Fact Dade_subproof (alpha : 'CF(L)) :
-  is_class_fun <<G>> [ffun x => oapp alpha 0 [pick a in A | x \in dd1 a]].
-Proof.
-rewrite genGid; apply: intro_class_fun => [x y Gx Gy | x notGx].
-  congr (oapp _ _); apply: eq_pick => a; rewrite memJ_norm //.
-  by apply: subsetP Gy; apply: class_support_norm.
-case: pickP => // a /andP[Aa Ha_u].
-by rewrite (subsetP Dade_support_sub) // in notGx; apply/bigcupP; exists a.
-Qed.
-Definition Dade alpha := Cfun 1 (Dade_subproof alpha).
-
-Lemma Dade_is_linear : linear Dade.
-Proof.
-move=> mu alpha beta; apply/cfunP=> x; rewrite !cfunElock.
-by case: pickP => [a _ | _] /=; rewrite ?mulr0 ?addr0 ?cfunE.
-Qed.
-Canonical Dade_additive := Additive Dade_is_linear.
-Canonical Dade_linear := Linear Dade_is_linear.
-
-Local Notation "alpha ^\tau" := (Dade alpha).
-
-(* This is the validity of Peterfalvi, Definition (2.5) *)
-Lemma DadeE alpha a u : a \in A -> u \in dd1 a -> alpha^\tau u = alpha a.
-Proof.
-move=> Aa Ha_u; rewrite cfunElock.
-have [b /= /andP[Ab Hb_u] | ] := pickP; last by move/(_ a); rewrite Aa Ha_u.
-have [|x Lx ->] := Dade_support1_TI Aa Ab; last by rewrite cfunJ.
-by apply/pred0Pn; exists u; rewrite /= Ha_u.
-Qed.
-
-Lemma Dade_id alpha : {in A, forall a, alpha^\tau a = alpha a}.
-Proof.
-by move=> a Aa; rewrite /= -{1}[a]mul1g (DadeE _ Aa) ?mem_Dade_support1.
-Qed.
-
-Lemma Dade_cfunS alpha : alpha^\tau \in 'CF(G, Atau).
-Proof.
-apply/cfun_onP=> x; rewrite cfunElock.
-by case: pickP => [a /andP[Aa Ha_x] /bigcupP[] | //]; exists a.
-Qed.
-
-Lemma Dade_cfun alpha : alpha^\tau \in 'CF(G, G^#).
-Proof. by rewrite (cfun_onS Dade_support_subD1) ?Dade_cfunS. Qed.
-
-Lemma Dade1 alpha : alpha^\tau 1%g = 0.
-Proof. by rewrite (cfun_on0 (Dade_cfun _)) // !inE eqxx. Qed.
-
-Lemma Dade_id1 :
-  {in 'CF(L, A) & 1%g |: A, forall alpha a, alpha^\tau a = alpha a}.
-Proof.
-move=> alpha a Aalpha; case/setU1P=> [-> |]; last exact: Dade_id.
-by rewrite Dade1 (cfun_on0 Aalpha).
-Qed.
-
-Section AutomorphismCFun.
-
-Variable u : {rmorphism algC -> algC}.
-Local Notation "alpha ^u" := (cfAut u alpha).
-
-Lemma Dade_aut alpha : (alpha^u)^\tau = (alpha^\tau)^u.
-Proof.
-apply/cfunP => g; rewrite cfunE.
-have [/bigcupP[a Aa A1g] | notAtau_g] := boolP (g \in Atau).
-  by rewrite !(DadeE _ Aa A1g) cfunE.
-by rewrite !(cfun_on0 _ notAtau_g) ?rmorph0 ?Dade_cfunS.
-Qed.
-
-End AutomorphismCFun.
-
-Lemma Dade_conjC alpha : (alpha^*)^\tau = ((alpha^\tau)^*)%CF.
-Proof. exact: Dade_aut. Qed.
-
-(* This is Peterfalvi (2.7), main part *)
-Lemma general_Dade_reciprocity alpha (phi : 'CF(G)) (psi : 'CF(L)) :
-    alpha \in 'CF(L, A) ->
-  {in A, forall a, psi a = #|H a|%:R ^-1 * (\sum_(x in H a) phi (x * a)%g)} ->
-  '[alpha^\tau, phi] = '[alpha, psi].
-Proof.
-move=> CFalpha psiA; rewrite (cfdotEl _ (Dade_cfunS _)).
-pose T := [set repr (a ^: L) | a in A].
-have sTA: {subset T <= A}.
-  move=> _ /imsetP[a Aa ->]; have [x Lx ->] := repr_class L a.
-  by rewrite memJ_norm ?(subsetP nAL).
-pose P_G := [set dd1 x | x in T].
-have dd1_id: {in A, forall a, dd1 (repr (a ^: L)) = dd1 a}.
-  by move=> a Aa /=; have [x Lx ->] := repr_class L a; apply: Dade_support1_id.
-have ->: Atau = cover P_G.
-  apply/setP=> u; apply/bigcupP/bigcupP=> [[a Aa Fa_u] | [Fa]]; last first.
-    by case/imsetP=> a /sTA Aa -> Fa_u; exists a.
-  by exists (dd1 a) => //; rewrite -dd1_id //; do 2!apply: mem_imset.
-have [tiP_G inj_dd1]: trivIset P_G /\ {in T &, injective dd1}.
-  apply: trivIimset => [_ _ /imsetP[a Aa ->] /imsetP[b Ab ->] |]; last first.
-    apply/imsetP=> [[a]]; move/sTA=> Aa; move/esym; move/eqP; case/set0Pn.
-    by exists (a ^ 1)%g; apply: mem_imset2; rewrite ?group1 ?rcoset_refl.
-  rewrite !dd1_id //; apply: contraR.
-  by case/Dade_support1_TI=> // x Lx ->; rewrite classGidl.
-rewrite big_trivIset //= big_imset {P_G tiP_G inj_dd1}//=.
-symmetry; rewrite (cfdotEl _ CFalpha).
-pose P_A := [set a ^: L | a in T].
-have rLid x: repr (x ^: L) ^: L = x ^: L.
-  by have [y Ly ->] := repr_class L x; rewrite classGidl.
-have {1}<-: cover P_A = A.
-  apply/setP=> a; apply/bigcupP/idP=> [[_ /imsetP[d /sTA Ab ->]] | Aa].
-    by case/imsetP=> x Lx ->; rewrite memJ_norm ?(subsetP nAL).
-  by exists (a ^: L); rewrite ?class_refl // -rLid; do 2!apply: mem_imset.
-have [tiP_A injFA]: trivIset P_A /\ {in T &, injective (class^~ L)}.
-  apply: trivIimset => [_ _ /imsetP[a Aa ->] /imsetP[b Ab ->] |]; last first.
-    by apply/imsetP=> [[a _ /esym/eqP/set0Pn[]]]; exists a; apply: class_refl.
-  rewrite !rLid; apply: contraR => /pred0Pn[c /andP[/=]].
-  by do 2!move/class_eqP <-.
-rewrite big_trivIset //= big_imset {P_A tiP_A injFA}//=.
-apply: canRL (mulKf (neq0CG G)) _; rewrite mulrA big_distrr /=.
-apply: eq_bigr => a /sTA=> {T sTA}Aa.
-have [La def_Ca] := (subsetP sAL a Aa, defCA Aa).
-rewrite (eq_bigr (fun _ => alpha a * (psi a)^*)) => [|ax]; last first.
-  by case/imsetP=> x Lx ->{ax}; rewrite !cfunJ.
-rewrite sumr_const -index_cent1 mulrC -mulr_natr -!mulrA.
-rewrite (eq_bigr (fun xa => alpha a * (phi xa)^*)) => [|xa Fa_xa]; last first.
-  by rewrite (DadeE _ Aa).
-rewrite -big_distrr /= -rmorph_sum; congr (_ * _).
-rewrite mulrC mulrA -natrM mulnC -(Lagrange (subsetIl G 'C[a])).
-rewrite -mulnA mulnCA -(sdprod_card def_Ca) -mulnA Lagrange ?subsetIl //.
-rewrite mulnA natrM mulfK ?neq0CG // -conjC_nat -rmorphM; congr (_ ^*).
-have /and3P[_ tiHa _] := Dade_cover_TI Aa.
-rewrite (set_partition_big _ (partition_class_support _ _)) //=.
-rewrite (eq_bigr (fun _ => \sum_(x in H a) phi (x * a)%g)); last first.
-  move=> _ /imsetP[x Gx ->]; rewrite -rcosetE.
-  rewrite (big_imset _ (in2W (conjg_inj x))) (big_imset _ (in2W (mulIg a))) /=.
-  by apply: eq_bigr => u Hu; rewrite cfunJ ?groupM ?(subsetP sLG a).
-rewrite sumr_const card_orbit astab1Js norm_Dade_cover //.
-by rewrite natrM -mulrA mulr_natl psiA // mulVKf ?neq0CG.
-Qed.
-
-(* This is Peterfalvi (2.7), second part. *)
-Lemma Dade_reciprocity alpha (phi : 'CF(G)) :
-    alpha \in 'CF(L, A) ->
-    {in A, forall a, {in H a, forall u, phi (u * a)%g = phi a}} ->
-  '[alpha^\tau, phi] = '[alpha, 'Res[L] phi].
-Proof.
-move=> CFalpha phiH; apply: general_Dade_reciprocity => // a Aa.
-rewrite cfResE ?(subsetP sAL) //; apply: canRL (mulKf (neq0CG _)) _.
-by rewrite mulr_natl -sumr_const; apply: eq_bigr => x Hx; rewrite phiH.
-Qed.
-
-(* This is Peterfalvi (2.6)(a). *)
-Lemma Dade_isometry : {in 'CF(L, A) &, isometry Dade}.
-Proof.
-move=> alpha beta CFalpha CFbeta /=.
-rewrite Dade_reciprocity ?Dade_cfun => // [|a Aa u Hu]; last first.
-  by rewrite (DadeE _ Aa) ?mem_Dade_support1 ?Dade_id.
-rewrite !(cfdotEl _ CFalpha); congr (_ * _); apply: eq_bigr => x Ax.
-by rewrite cfResE ?(subsetP sAL) // Dade_id.
-Qed.
-
-(* Supplement to Peterfalvi (2.3)/(2.6)(a); implies Isaacs Lemma 7.7. *)
-Lemma Dade_Ind : normedTI A G L -> {in 'CF(L, A), Dade =1 'Ind}.
-Proof.
-case/Dade_normedTI_P=> _ trivH alpha Aalpha.
-rewrite [alpha^\tau]cfun_sum_cfdot ['Ind _]cfun_sum_cfdot.
-apply: eq_bigr => i _; rewrite -cfdot_Res_r -Dade_reciprocity // => a Aa /= u.
-by rewrite trivH // => /set1P->; rewrite mul1g.
-Qed.
-
-Definition Dade_set_signalizer (B : {set gT}) := \bigcap_(a in B) H a.
-Local Notation "''H' ( B )" := (Dade_set_signalizer B)
-  (at level 8, format "''H' ( B )") : group_scope.
-Canonical Dade_set_signalizer_group B := [group of 'H(B)].
-Definition Dade_set_normalizer B := 'H(B) <*> 'N_L(B).
-Local Notation "''M' ( B )" := (Dade_set_normalizer B)
-  (at level 8, format "''M' ( B )") : group_scope.
-Canonical Dade_set_normalizer_group B := [group of 'M(B)].
-
-Let calP := [set B : {set gT} | B \subset A & B != set0].
-
-(* This is Peterfalvi (2.8). *)
-Lemma Dade_set_sdprod : {in calP, forall B, 'H(B) ><| 'N_L(B) = 'M(B)}.
-Proof.
-move=> B /setIdP[sBA notB0]; apply: sdprodEY => /=.
-  apply/subsetP=> x /setIP[Lx nBx]; rewrite inE.
-  apply/bigcapsP=> a Ba; have Aa := subsetP sBA a Ba.
-  by rewrite sub_conjg -DadeJ ?groupV // bigcap_inf // memJ_norm ?groupV.
-have /set0Pn[a Ba] := notB0; have Aa := subsetP sBA a Ba.
-have [_ /mulG_sub[sHaC _] _ tiHaL] := sdprodP (defCA Aa).
-rewrite -(setIidPl sLG) -setIA setICA (setIidPl sHaC) in tiHaL.
-by rewrite setICA ['H(B)](bigD1 a) //= !setIA tiHaL !setI1g.
-Qed.
-
-Section DadeExpansion.
-
-Variable aa : 'CF(L).
-Hypothesis CFaa : aa \in 'CF(L, A).
-
-Definition Dade_restrm B :=
-  if B \in calP then remgr 'H(B) 'N_L(B) else trivm 'M(B).
-Fact Dade_restrM B : {in 'M(B) &, {morph Dade_restrm B : x y / x * y}%g}.
-Proof.
-rewrite /Dade_restrm; case: ifP => calP_B; last exact: morphM.
-have defM := Dade_set_sdprod calP_B; have [nsHM _ _ _ _] := sdprod_context defM.
-by apply: remgrM; first apply: sdprod_compl.
-Qed.
-Canonical Dade_restr_morphism B := Morphism (@Dade_restrM B).
-Definition Dade_cfun_restriction B :=
-  cfMorph ('Res[Dade_restrm B @* 'M(B)] aa).
-
-Local Notation "''aa_' B" := (Dade_cfun_restriction B)
-  (at level 3, B at level 2, format "''aa_' B") : ring_scope.
-
-Definition Dade_transversal := [set repr (B :^: L) | B in calP].
-Local Notation calB := Dade_transversal.
-
-Lemma Dade_restrictionE B x :
-  B \in calP -> 'aa_B x = aa (remgr 'H(B) 'N_L(B) x) *+ (x \in 'M(B)).
-Proof.
-move=> calP_B; have /sdprodP[_ /= defM _ _] := Dade_set_sdprod calP_B.
-have [Mx | /cfun0-> //] := boolP (x \in 'M(B)).
-rewrite mulrb cfMorphE // morphimEdom /= /Dade_restrm calP_B.
-rewrite cfResE ?mem_imset {x Mx}//= -defM.
-by apply/subsetP=> _ /imsetP[x /mem_remgr/setIP[Lx _] ->].
-Qed.
-Local Notation rDadeE := Dade_restrictionE.
-
-Lemma Dade_restriction_vchar B : aa \in 'Z[irr L] -> 'aa_B \in 'Z[irr 'M(B)].
-Proof.
-rewrite /'aa_B => /vcharP[a1 Na1 [a2 Na2 ->]].
-by rewrite !linearB /= rpredB // char_vchar ?cfMorph_char ?cfRes_char.
-Qed.
-
-Let sMG B : B \in calP -> 'M(B) \subset G.
-Proof.
-case/setIdP=> /subsetP sBA /set0Pn[a Ba].
-by rewrite join_subG ['H(B)](bigD1 a Ba) !subIset ?sLG ?sHG ?sBA.
-Qed.
-
-(* This is Peterfalvi (2.10.1) *)
-Lemma Dade_Ind_restr_J :
-  {in L & calP, forall x B, 'Ind[G] 'aa_(B :^ x) = 'Ind[G] 'aa_B}.
-Proof.
-move=> x B Lx dB; have [defMB [sBA _]] := (Dade_set_sdprod dB, setIdP dB).
-have dBx: B :^ x \in calP.
-  by rewrite !inE -{2}(normsP nAL x Lx) conjSg -!cards_eq0 cardJg in dB *.
-have defHBx: 'H(B :^ x) = 'H(B) :^ x.
-  rewrite /'H(_) (big_imset _ (in2W (conjg_inj x))) -bigcapJ /=.
-  by apply: eq_bigr => a Ba; rewrite DadeJ ?(subsetP sBA).
-have defNBx: 'N_L(B :^ x) = 'N_L(B) :^ x by rewrite conjIg -normJ (conjGid Lx).
-have [_ mulHNB _ tiHNB] := sdprodP defMB.
-have defMBx: 'M(B :^ x) = 'M(B) :^ x.
-  rewrite -mulHNB conjsMg -defHBx -defNBx.
-  by case/sdprodP: (Dade_set_sdprod dBx).
-have def_aa_x y: 'aa_(B :^ x) (y ^ x) = 'aa_B y.
-  rewrite !rDadeE // defMBx memJ_conjg !mulrb -mulHNB defHBx defNBx.
-  have [[h z Hh Nz ->] | // ] := mulsgP.
-  by rewrite conjMg !remgrMid ?cfunJ ?memJ_conjg // -conjIg tiHNB conjs1g.
-apply/cfunP=> y; have Gx := subsetP sLG x Lx.
-rewrite [eq]lock !cfIndE ?sMG //= {1}defMBx cardJg -lock; congr (_ * _).
-rewrite (reindex_astabs 'R x) ?astabsR //=.
-by apply: eq_bigr => z _; rewrite conjgM def_aa_x.
-Qed.
-
-(* This is Peterfalvi (2.10.2) *)
-Lemma Dade_setU1 : {in calP & A, forall B a, 'H(a |: B) = 'C_('H(B))[a]}.
-Proof.
-move=> B a dB Aa; rewrite /'H(_) bigcap_setU big_set1 -/'H(B).
-apply/eqP; rewrite setIC eqEsubset setIS // subsetI subsetIl /=.
-have [sHBG pi'HB]: 'H(B) \subset G /\ pi^'.-group 'H(B).
-  have [sBA /set0Pn[b Bb]] := setIdP dB; have Ab := subsetP sBA b Bb.
-  have sHBb: 'H(B) \subset H b by rewrite ['H(B)](bigD1 b) ?subsetIl.
-  by rewrite (pgroupS sHBb) ?pi'H ?(subset_trans sHBb) ?sHG.
-have [nsHa _ defCa _ _] := sdprod_context (defCA Aa).
-have [hallHa _] := coprime_mulGp_Hall defCa (pi'H a) (piCL Aa).
-by rewrite (sub_normal_Hall hallHa) ?(pgroupS (subsetIl _ _)) ?setSI.
-Qed.
-
-Let calA g (X : {set gT}) := [set x in G | g ^ x \in X]%g.
-
-(* This is Peterfalvi (2.10.3) *)
-Lemma Dade_Ind_expansion B g :
-    B \in calP ->
-  [/\ g \notin Atau -> ('Ind[G, 'M(B)] 'aa_B) g = 0
-    & {in A, forall a, g \in dd1 a ->
-       ('Ind[G, 'M(B)] 'aa_B) g =
-          (aa a / #|'M(B)|%:R) *
-               \sum_(b in 'N_L(B) :&: a ^: L) #|calA g ('H(B) :* b)|%:R}].
-Proof.
-move=> dB; set LHS := 'Ind _ g.
-have defMB := Dade_set_sdprod dB; have [_ mulHNB nHNB tiHNB] := sdprodP defMB.
-have [sHMB sNMB] := mulG_sub mulHNB.
-have{LHS} ->: LHS = #|'M(B)|%:R^-1 * \sum_(x in calA g 'M(B)) 'aa_B (g ^ x).
-  rewrite {}/LHS cfIndE ?sMG //; congr (_ * _).
-  rewrite (bigID [pred x | g ^ x \in 'M(B)]) /= addrC big1 ?add0r => [|x].
-    by apply: eq_bigl => x; rewrite inE.
-  by case/andP=> _ notMgx; rewrite cfun0.
-pose fBg x := remgr 'H(B) 'N_L(B) (g ^ x).
-pose supp_aBg := [pred b in A | g \in dd1 b].
-have supp_aBgP: {in calA g 'M(B), forall x,
-  ~~ supp_aBg (fBg x) -> 'aa_B (g ^ x)%g = 0}.
-- move=> x /setIdP[]; set b := fBg x => Gx MBgx notHGx; rewrite rDadeE // MBgx.
-  have Nb: b \in 'N_L(B) by rewrite mem_remgr ?mulHNB.
-  have Cb: b \in 'C_L[b] by rewrite inE cent1id; have [-> _] := setIP Nb.
-  rewrite (cfun_on0 CFaa) // -/(fBg x) -/b; apply: contra notHGx => Ab.
-  have nHb: b \in 'N('H(B)) by rewrite (subsetP nHNB).
-  have [sBA /set0Pn[a Ba]] := setIdP dB; have Aa := subsetP sBA a Ba.
-  have [|/= partHBb _] := partition_cent_rcoset nHb.
-    rewrite (coprime_dvdr (order_dvdG Cb)) //= ['H(B)](bigD1 a) //=.
-    by rewrite (coprimeSg (subsetIl _ _)) ?coHL.
-  have Hb_gx: g ^ x \in 'H(B) :* b by rewrite mem_rcoset mem_divgr ?mulHNB.
-  have [defHBb _ _] := and3P partHBb; rewrite -(eqP defHBb) in Hb_gx.
-  case/bigcupP: Hb_gx => Cy; case/imsetP=> y HBy ->{Cy} Cby_gx.
-  have sHBa: 'H(B) \subset H a by rewrite bigcap_inf.
-  have sHBG: 'H(B) \subset G := subset_trans sHBa (sHG a).
-  rewrite Ab -(memJ_conjg _ x) class_supportGidr //  -(conjgKV y (g ^ x)).
-  rewrite mem_imset2 // ?(subsetP sHBG) {HBy}// -mem_conjg.
-  apply: subsetP Cby_gx; rewrite {y}conjSg mulSg //.
-  have [nsHb _ defCb _ _] := sdprod_context (defCA Ab).
-  have [hallHb _] := coprime_mulGp_Hall defCb (pi'H b) (piCL Ab).
-  rewrite (sub_normal_Hall hallHb) ?setSI // (pgroupS _ (pi'H a)) //=.
-  by rewrite subIset ?sHBa.
-split=> [notHGg | a Aa Hag].
-  rewrite big1 ?mulr0 // => x; move/supp_aBgP; apply; set b := fBg x.
-  by apply: contra notHGg; case/andP=> Ab Hb_x; apply/bigcupP; exists b.
-rewrite -mulrA mulrCA; congr (_ * _); rewrite big_distrr /=.
-set nBaL := _ :&: _; rewrite (bigID [pred x | fBg x \in nBaL]) /= addrC.
-rewrite big1 ?add0r => [|x /andP[calAx not_nBaLx]]; last first.
-  apply: supp_aBgP => //; apply: contra not_nBaLx.
-  set b := fBg x => /andP[Ab Hb_g]; have [Gx MBx] := setIdP calAx.
-  rewrite inE mem_remgr ?mulHNB //; apply/imsetP/Dade_support1_TI => //.
-  by apply/pred0Pn; exists g; apply/andP.
-rewrite (partition_big fBg (mem nBaL)) /= => [|x]; last by case/andP.
-apply: eq_bigr => b; case/setIP=> Nb aLb; rewrite mulr_natr -sumr_const.
-apply: eq_big => x; rewrite ![x \in _]inE -!andbA.
-  apply: andb_id2l=> Gx; apply/and3P/idP=> [[Mgx _] /eqP <- | HBb_gx].
-    by rewrite mem_rcoset mem_divgr ?mulHNB.
-  suffices ->: fBg x = b.
-    by rewrite inE Nb (subsetP _ _ HBb_gx) // -mulHNB mulgS ?sub1set.
-  by rewrite /fBg; have [h Hh ->] := rcosetP HBb_gx; apply: remgrMid.
-move/and4P=> [_ Mgx _ /eqP def_fx].
-rewrite rDadeE // Mgx -/(fBg x) def_fx; case/imsetP: aLb => y Ly ->.
-by rewrite cfunJ // (subsetP sAL).
-Qed.
-
-(* This is Peterfalvi (2.10) *)
-Lemma Dade_expansion :
-  aa^\tau = - \sum_(B in calB) (- 1) ^+ #|B| *: 'Ind[G, 'M(B)] 'aa_B.
-Proof.
-apply/cfunP=> g; rewrite !cfunElock sum_cfunE.
-pose n1 (B : {set gT}) : algC := (-1) ^+ #|B| / #|L : 'N_L(B)|%:R.
-pose aa1 B := ('Ind[G, 'M(B)] 'aa_B) g.
-have dBJ: {acts L, on calP | 'Js}.
-  move=> x Lx /= B; rewrite !inE -!cards_eq0 cardJg.
-  by rewrite -{1}(normsP nAL x Lx) conjSg.
-transitivity (- (\sum_(B in calP) n1 B * aa1 B)); last first.
-  congr (- _); rewrite {1}(partition_big_imset (fun B => repr (B :^: L))) /=.
-  apply: eq_bigr => B /imsetP[B1 dB1 defB].
-  have B1L_B: B \in B1 :^: L by rewrite defB (mem_repr B1) ?orbit_refl.
-  have{dB1} dB1L: {subset B1 :^: L <= calP}.
-    by move=> _ /imsetP[x Lx ->]; rewrite dBJ.
-  have dB: B \in calP := dB1L B B1L_B.
-  rewrite (eq_bigl (mem (B :^: L))) => [|B2 /=]; last first.
-    apply/andP/idP=> [[_ /eqP <-] | /orbit_trans/(_ B1L_B)-B1L_B2].
-      by rewrite orbit_sym (mem_repr B2) ?orbit_refl.
-    by rewrite [B2 :^: L](orbit_eqP B1L_B2) -defB dB1L.
-  rewrite (eq_bigr (fun _ => n1 B * aa1 B)) => [|_ /imsetP[x Lx ->]].
-    rewrite cfunE sumr_const -mulr_natr mulrAC card_orbit astab1Js divfK //.
-    by rewrite pnatr_eq0 -lt0n indexg_gt0.
-  rewrite /aa1 Dade_Ind_restr_J //; congr (_ * _).
-  by rewrite /n1 cardJg -{1 2}(conjGid Lx) normJ -conjIg indexJg.
-case: pickP => /= [a /andP[Aa Ha_g] | notHAg]; last first.
-  rewrite big1 ?oppr0 // /aa1 => B dB.
-  have [->] := Dade_Ind_expansion g dB; first by rewrite mulr0.
-  by apply/bigcupP=> [[a Aa Ha_g]]; case/andP: (notHAg a).
-pose P_ b := [set B in calP | b \in 'N_L(B)].
-pose aa2 B b : algC := #|calA g ('H(B) :* b)|%:R.
-pose nn2 (B : {set gT}) : algC := (-1) ^+ #|B| / #|'H(B)|%:R.
-pose sumB b := \sum_(B in P_ b) nn2 B * aa2 B b.
-transitivity (- aa a / #|L|%:R * \sum_(b in a ^: L) sumB b); last first.
-  rewrite !mulNr; congr (- _).
-  rewrite (exchange_big_dep (mem calP)) => [|b B _] /=; last by case/setIdP.
-  rewrite big_distrr /aa1; apply: eq_bigr => B dB; rewrite -big_distrr /=.
-  have [_ /(_ a) -> //] := Dade_Ind_expansion g dB; rewrite !mulrA.
-  congr (_ * _); last by apply: eq_bigl => b; rewrite inE dB /= andbC -in_setI.
-  rewrite -mulrA mulrCA -!mulrA; congr (_ * _).
-  rewrite -invfM mulrCA -invfM -!natrM; congr (_ / _%:R).
-  rewrite -(sdprod_card (Dade_set_sdprod dB)) mulnA mulnAC; congr (_ * _)%N.
-  by rewrite mulnC Lagrange ?subsetIl.
-rewrite (eq_bigr (fun _ => sumB a)) /= => [|_ /imsetP[x Lx ->]]; last first.
-  rewrite {1}/sumB (reindex_inj (@conjsg_inj _ x)) /=.
-  symmetry; apply: eq_big => B.
-    rewrite ![_ \in P_ _]inE dBJ //.
-    by rewrite -{2}(conjGid Lx) normJ -conjIg memJ_conjg.
-  case/setIdP=> dB Na; have [sBA _] := setIdP dB.
-  have defHBx: 'H(B :^ x) = 'H(B) :^ x.
-    rewrite /'H(_) (big_imset _ (in2W (conjg_inj x))) -bigcapJ /=.
-    by apply: eq_bigr => b Bb; rewrite DadeJ ?(subsetP sBA).
-  rewrite /nn2 /aa2 defHBx !cardJg; congr (_ * _%:R).
-  rewrite -(card_rcoset _ x); apply: eq_card => y.
-  rewrite !(inE, mem_rcoset, mem_conjg) conjMg conjVg conjgK -conjgM.
-  by rewrite groupMr // groupV (subsetP sLG).
-rewrite sumr_const mulrC [sumB a](bigD1 [set a]) /=; last first.
-  by rewrite 3!inE cent1id sub1set Aa -cards_eq0 cards1 (subsetP sAL).
-rewrite -[_ *+ _]mulr_natr -mulrA mulrDl -!mulrA ['H(_)]big_set1 cards1.
-have ->: aa2 [set a] a = #|'C_G[a]|%:R.
-  have [u x Ha_ux Gx def_g] := imset2P Ha_g.
-  rewrite -(card_lcoset _ x^-1); congr _%:R; apply: eq_card => y.
-  rewrite ['H(_)]big_set1 mem_lcoset invgK inE def_g -conjgM.
-  rewrite -(groupMl y Gx) inE; apply: andb_id2l => Gxy.
-  by have [_ _ -> //] := normedTI_memJ_P (Dade_cover_TI Aa); rewrite inE Gxy.
-rewrite mulN1r mulrC mulrA -natrM -(sdprod_card (defCA Aa)).
-rewrite -mulnA card_orbit astab1J Lagrange ?subsetIl // mulnC natrM.
-rewrite mulrAC mulfK ?neq0CG // mulrC divfK ?neq0CG // opprK.
-rewrite (bigID [pred B : {set gT} | a \in B]) /= mulrDl addrA.
-apply: canRL (subrK _) _; rewrite -mulNr -sumrN; congr (_ + _ * _).
-symmetry.
-rewrite (reindex_onto (fun B => a |: B) (fun B => B :\ a)) /=; last first.
-  by move=> B; case/andP=> _; apply: setD1K.
-symmetry; apply: eq_big => B.
-  rewrite setU11 andbT -!andbA; apply/and3P/and3P; case.
-    do 2![case/setIdP] => sBA ntB /setIP[La nBa] _ notBa.
-    rewrite 3!inE subUset sub1set Aa sBA La setU1K // -cards_eq0 cardsU1 notBa.
-    rewrite -sub1set normsU ?sub1set ?cent1id //= eq_sym eqEcard subsetUl /=.
-    by rewrite cards1 cardsU1 notBa ltnS leqn0 cards_eq0.
-  do 2![case/setIdP] => /subUsetP[_ sBA] _ /setIP[La].
-  rewrite inE conjUg (normP (cent1id a)) => /subUsetP[_ sBa_aB].
-  rewrite eq_sym eqEcard subsetUl cards1 (cardsD1 a) setU11 ltnS leqn0 /=.
-  rewrite cards_eq0 => notB0 /eqP defB.
-  have notBa: a \notin B by rewrite -defB setD11.
-  split=> //; last by apply: contraNneq notBa => ->; apply: set11.
-  rewrite !inE sBA La -{1 3}defB notB0 subsetD1 sBa_aB.
-  by rewrite mem_conjg /(a ^ _) invgK mulgA mulgK.
-do 2![case/andP] => /setIdP[dB Na] _ notBa.
-suffices ->: aa2 B a = #|'H(B) : 'H(a |: B)|%:R * aa2 (a |: B) a.
-  rewrite /nn2 cardsU1 notBa exprS mulN1r !mulNr; congr (- _).
-  rewrite !mulrA; congr (_ * _); rewrite -!mulrA; congr (_ * _).
-  apply: canLR (mulKf (neq0CG _)) _; apply: canRL (mulfK (neq0CG _)) _ => /=.
-  by rewrite -natrM mulnC Lagrange //= Dade_setU1 ?subsetIl.
-rewrite /aa2 Dade_setU1 //= -natrM; congr _%:R.
-have defMB := Dade_set_sdprod dB; have [_ mulHNB nHNB tiHNB] := sdprodP defMB.
-have [sHMB sNMB] := mulG_sub mulHNB; have [La nBa] := setIP Na.
-have nHa: a \in 'N('H(B)) by rewrite (subsetP nHNB).
-have Ca: a \in 'C_L[a] by rewrite inE cent1id La.
-have [|/= partHBa nbHBa] := partition_cent_rcoset nHa.
-  have [sBA] := setIdP dB; case/set0Pn=> b Bb; have Ab := subsetP sBA b Bb.
-  rewrite (coprime_dvdr (order_dvdG Ca)) //= ['H(B)](bigD1 b) //=.
-  by rewrite (coprimeSg (subsetIl _ _)) ?coHL.
-pose pHBa := mem ('H(B) :* a).
-rewrite -sum1_card (partition_big (fun x => g ^ x) pHBa) /= => [|x]; last first.
-  by case/setIdP=> _ ->.
-rewrite (set_partition_big _ partHBa) /= -nbHBa -sum_nat_const.
-apply: eq_bigr => _ /imsetP[x Hx ->].
-rewrite (big_imset _ (in2W (conjg_inj x))) /=.
-rewrite -(card_rcoset _ x) -sum1_card; symmetry; set HBaa := 'C_(_)[a] :* a.
-rewrite (partition_big (fun y => g ^ (y * x^-1)) (mem HBaa)); last first.
-  by move=> y; rewrite mem_rcoset => /setIdP[].
-apply: eq_bigr => /= u Ca_u; apply: eq_bigl => z.
-rewrite -(canF_eq (conjgKV x)) -conjgM; apply: andb_id2r; move/eqP=> def_u.
-have sHBG: 'H(B) \subset G.
-  have [sBA /set0Pn[b Bb]] := setIdP dB; have Ab := subsetP sBA b Bb.
-  by rewrite (bigcap_min b) ?sHG.
-rewrite mem_rcoset !inE groupMr ?groupV ?(subsetP sHBG x Hx) //=.
-congr (_ && _); have [/eqP defHBa _ _] := and3P partHBa.
-symmetry; rewrite def_u Ca_u -defHBa -(mulgKV x z) conjgM def_u -/HBaa.
-by rewrite cover_imset -class_supportEr mem_imset2.
-Qed.
-
-End DadeExpansion.
-
-(* This is Peterfalvi (2.6)(b) *)
-Lemma Dade_vchar alpha : alpha \in 'Z[irr L, A] -> alpha^\tau \in 'Z[irr G].
-Proof.
-rewrite [alpha \in _]zchar_split => /andP[Zaa CFaa].
-rewrite Dade_expansion // rpredN rpred_sum // => B dB.
-suffices calP_B: B \in calP.
-  by rewrite rpredZsign cfInd_vchar // Dade_restriction_vchar.
-case/imsetP: dB => B0 /setIdP[sB0A notB00] defB.
-have [x Lx ->]: exists2 x, x \in L & B = B0 :^ x.
-  by apply/imsetP; rewrite defB (mem_repr B0) ?orbit_refl.
-by rewrite inE -cards_eq0 cardJg cards_eq0 -(normsP nAL x Lx) conjSg sB0A.
-Qed.
-
-(* This summarizes Peterfalvi (2.6). *)
-Lemma Dade_Zisometry : {in 'Z[irr L, A], isometry Dade, to 'Z[irr G, G^#]}.
-Proof.
-split; first by apply: sub_in2 Dade_isometry; apply: zchar_on.
-by move=> phi Zphi; rewrite /= zchar_split Dade_vchar ?Dade_cfun.
-Qed.
-
-End Two.
-
-Section RestrDade.
-
-Variables (gT : finGroupType) (G L : {group gT}) (A A1 : {set gT}).
-Hypothesis ddA : Dade_hypothesis G L A.
-Hypotheses (sA1A : A1 \subset A) (nA1L : L \subset 'N(A1)).
-Let ssA1A := subsetP sA1A.
-
-(* This is Peterfalvi (2.11), first part. *)
-Lemma restr_Dade_hyp : Dade_hypothesis G L A1.
-Proof.
-have [/andP[sAL nAL] notA_1 sLG conjAG [H defCa coHL]] := ddA.
-have nsA1L: A1 <| L by rewrite /normal (subset_trans sA1A).
-split; rewrite ?(contra (@ssA1A _)) //; first exact: sub_in2 conjAG.
-by exists H; [apply: sub_in1 defCa | apply: sub_in2 coHL].
-Qed.
-Local Notation ddA1 := restr_Dade_hyp.
-
-Local Notation H dd := (Dade_signalizer dd).
-Lemma restr_Dade_signalizer H1 : {in A, H ddA =1 H1} -> {in A1, H ddA1 =1 H1}.
-Proof.
-move=> defH1; apply: def_Dade_signalizer => a /ssA1A Aa.
-by rewrite -defH1 ?Dade_sdprod.
-Qed.
-
-Lemma restr_Dade_support1 : {in A1, Dade_support1 ddA1 =1 Dade_support1 ddA}.
-Proof.
-by move=> a A1a; rewrite /Dade_support1 (@restr_Dade_signalizer (H ddA)).
-Qed.
-
-Lemma restr_Dade_support :
-  Dade_support ddA1 = \bigcup_(a in A1) Dade_support1 ddA a.
-Proof. by rewrite -(eq_bigr _ restr_Dade_support1). Qed.
-
-Definition restr_Dade := Dade ddA1.
-
-(* This is Peterfalvi (2.11), second part. *)
-Lemma restr_DadeE : {in 'CF(L, A1), restr_Dade =1 Dade ddA}.
-Proof.
-move=> aa CF1aa; apply/cfunP=> g; rewrite cfunElock.
-have CFaa: aa \in 'CF(L, A) := cfun_onS sA1A CF1aa.
-have [a /= /andP[A1a Ha_g] | no_a /=] := pickP.
-  by apply/esym/DadeE; rewrite -1?restr_Dade_support1 ?ssA1A.
-rewrite cfunElock; case: pickP => //= a /andP[_ Ha_g].
-rewrite (cfun_on0 CF1aa) //; apply: contraFN (no_a a) => A1a.
-by rewrite A1a restr_Dade_support1.
-Qed.
-
-End RestrDade.
-
-Section NormedTI.
-
-Variables (gT : finGroupType) (G L : {group gT}) (A : {set gT}).
-Hypotheses (tiAG : normedTI A G L) (sAG1 : A \subset G^#).
-
-(* This is the existence part of Peterfalvi (2.3). *)
-Lemma normedTI_Dade : Dade_hypothesis G L A.
-Proof.
-have [[sAG notA1] [_ _ /eqP defL]] := (subsetD1P sAG1, and3P tiAG).
-have [_ sLG tiAG_L] := normedTI_memJ_P tiAG.
-split=> // [|a b Aa Ab /imsetP[x Gx def_b]|].
-- rewrite /(A <| L) -{2}defL subsetIr andbT; apply/subsetP=> a Aa.
-  by rewrite -(tiAG_L a) ?(subsetP sAG) // conjgE mulKg.
-- by rewrite def_b mem_imset // -(tiAG_L a) -?def_b.
-exists (fun _ => 1%G) => [a Aa | a b _ _]; last by rewrite cards1 coprime1n.
-by rewrite sdprod1g -(setIidPl sLG) -setIA (setIidPr (cent1_normedTI tiAG Aa)).
-Qed.
-
-Let def_ddA := Dade_Ind normedTI_Dade tiAG.
-
-(* This is the identity part of Isaacs, Lemma 7.7. *)
-Lemma normedTI_Ind_id1 :
-  {in 'CF(L, A) & 1%g |: A, forall alpha, 'Ind[G] alpha =1 alpha}.
-Proof. by move=> aa a CFaa A1a; rewrite /= -def_ddA // Dade_id1. Qed.
-
-(* A more restricted, but more useful form. *)
-Lemma normedTI_Ind_id :
-  {in 'CF(L, A) & A, forall alpha, 'Ind[G] alpha =1 alpha}.
-Proof. by apply: sub_in11 normedTI_Ind_id1 => //; apply/subsetP/subsetUr. Qed.
-
-(* This is the isometry part of Isaacs, Lemma 7.7. *)
-(* The statement in Isaacs is slightly more general in that it allows for     *)
-(* beta \in 'CF(L, 1%g |: A); this appears to be more cumbersome than useful. *)
-Lemma normedTI_isometry : {in 'CF(L, A) &, isometry 'Ind[G]}.
-Proof. by move=> aa bb CFaa CFbb; rewrite /= -!def_ddA // Dade_isometry. Qed.
-
-End NormedTI.
\ No newline at end of file