diff options
| author | Cyril Cohen | 2017-11-23 16:33:36 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-02-06 13:54:37 +0100 |
| commit | fafd4dac5315e1d4e071b0044a50a16360b31964 (patch) | |
| tree | 5b66c3d67e2b146e3a8013496379b96dd60dc75a /mathcomp/odd_order | |
| parent | 835467324db450c8fb8971e477cc4d82fa3e861b (diff) | |
running semi-automated linting on the whole library
Diffstat (limited to 'mathcomp/odd_order')
33 files changed, 244 insertions, 244 deletions
diff --git a/mathcomp/odd_order/BGappendixAB.v b/mathcomp/odd_order/BGappendixAB.v index 1dc4472..eb708a6 100644 --- a/mathcomp/odd_order/BGappendixAB.v +++ b/mathcomp/odd_order/BGappendixAB.v @@ -73,7 +73,7 @@ suffices IH gT (E : {group gT}) x y (G := <<[set x; y]>>) : by rewrite -cRA !commgSS ?sub1set. move: {2}_.+1 (ltnSn #|E|) => n; elim: n => // n IHn in gT E x y G *. rewrite ltnS => leEn /and3P[oddG pE nEG] /and3P[/andP[p_x cRx] p_y cRy]. -have [Gx Gy]: x \in G /\ y \in G by apply/andP; rewrite -!sub1set -join_subG. +have [Gx Gy]: x \in G /\ y \in G by apply/andP; rewrite -!sub1set -join_subG. apply: wlog_neg => p'Gc; apply/pgroupP=> q q_pr qGc; apply/idPn => p'q. have [Q sylQ] := Sylow_exists q [group of G]. have [sQG qQ]: Q \subset G /\ q.-group Q by case/and3P: sylQ. @@ -130,7 +130,7 @@ case ncxy: (rG x *m rG y == rG y *m rG x). rewrite -defC inE groupR //= !repr_mxM ?groupM ?groupV // mul1mx -/rG. by rewrite (eqP ncxy) -!repr_mxM ?groupM ?groupV // mulKg mulVg repr_mx1. rewrite [_^`(1)](commG1P _) ?pgroup1 //= quotient_gen -gen_subG //= -/G. - rewrite !gen_subG centsC gen_subG quotient_cents2r ?gen_subG //= -/G. + rewrite !gen_subG centsC gen_subG quotient_cents2r ?gen_subG //= -/G. rewrite /commg_set imset2Ul !imset2_set1l !imsetU !imset_set1. by rewrite !subUset andbC !sub1set !commgg group1 /= -invg_comm groupV Cxy. pose Ax : 'M(E) := rG x - 1; pose Ay : 'M(E) := rG y - 1. @@ -231,7 +231,7 @@ Qed. Theorem odd_abelian_gen_constrained : 'O_p^'(G) = 1 -> 'C_('O_p(G))(P) \subset P -> X \subset 'O_p(G). Proof. -set Q := 'O_p(G) => p'G1 sCQ_P. +set Q := 'O_p(G) => p'G1 sCQ_P. have sPQ: P \subset Q by rewrite pcore_max. have defQ: 'O_{p^', p}(G) = Q by rewrite pseries_pop2. have pQ: p.-group Q by apply: pcore_pgroup. @@ -460,7 +460,7 @@ have sylCS: p.-Sylow(C) (C :&: S) := Sylow_setI_normal nsCG sylS. have{defC} defC: 'C_G(Y) * (C :&: S) = C. apply/eqP; rewrite eqEsubset mulG_subG sCY_C subsetIl /=. have nCY_C: C \subset 'N('C_G(Y)). - exact: subset_trans (normal_sub nsCG) (normal_norm nsCY_G). + exact: subset_trans (normal_sub nsCG) (normal_norm nsCY_G). rewrite -quotientSK // -defC /= -pseries1. rewrite -(pseries_catr_id [:: p : nat_pred]) (pseries_rcons_id [::]) /=. rewrite pseries1 /= pseries1 defC pcore_sub_Hall // morphim_pHall //. diff --git a/mathcomp/odd_order/BGappendixC.v b/mathcomp/odd_order/BGappendixC.v index f8b9137..3cfb101 100644 --- a/mathcomp/odd_order/BGappendixC.v +++ b/mathcomp/odd_order/BGappendixC.v @@ -370,7 +370,7 @@ have [q_gt4 | q_le4] := ltnP 4 q. rewrite natrM real_ler_distl ?rpredB ?rpredM ?rpred_nat // => /andP[lb_Pe _]. rewrite -ltC_nat -(ltr_pmul2l (gt0CG P)) {lb_Pe}(ltr_le_trans _ lb_Pe) //. rewrite ltr_subr_addl (@ler_lt_trans _ ((p ^ q.-1)%:R ^+ 2)) //; last first. - rewrite -!natrX ltC_nat ltn_sqr oU ltn_divRL ?dvdn_pred_predX //. + rewrite -!natrX ltC_nat ltn_sqr oU ltn_divRL ?dvdn_pred_predX //. rewrite -(subnKC qgt1) /= -!subn1 mulnBr muln1 -expnSr. by rewrite ltn_sub2l ?(ltn_exp2l 0) // prime_gt1. rewrite -mulrDr -natrX -expnM muln2 -subn1 doubleB -addnn -addnBA // subn2. diff --git a/mathcomp/odd_order/BGsection1.v b/mathcomp/odd_order/BGsection1.v index 7539af3..3230da2 100644 --- a/mathcomp/odd_order/BGsection1.v +++ b/mathcomp/odd_order/BGsection1.v @@ -148,7 +148,7 @@ apply/setIidPl/minM'; last exact: subsetIl. apply/andP; split; last by rewrite normsI // normal_norm. apply: meet_center_nil => //; first by apply: Fitting_nil. apply/andP; split; last exact: gFsub_trans. -apply: Fitting_max; rewrite // /normal ?sMG //; apply: abelian_nil. +apply: Fitting_max; rewrite // /normal ?sMG //; apply: abelian_nil. by move: (minnormal_solvable_abelem minM solM) => /abelem_abelian. Qed. @@ -426,7 +426,7 @@ have sCG: C \subset G by rewrite subsetIl. suffices cNA : A \subset 'C(N). rewrite centsC (sameP setIidPl eqP) -(nilpotent_sub_norm nilG sCG) //= -/C. by rewrite subsetI subsetIl centsC. -have{nilG} solN: solvable N by rewrite(solvableS sNG) ?nilpotent_sol. +have{nilG} solN: solvable N by rewrite (solvableS sNG) ?nilpotent_sol. rewrite (stable_factor_cent cCA) ?(coprimeSg sNG) /stable_factor //= -/N -/C. rewrite subcent_normal subsetI (subset_trans (commSg A sNG)) ?commg_subl //=. rewrite comm_norm_cent_cent 1?centsC ?subsetIr // normsI // !norms_norm //. @@ -636,7 +636,7 @@ have nKG: G \subset 'N(K) by rewrite normal_norm ?pcore_normal. have nKC: 'C_G(P) \subset 'N(K) by rewrite subIset ?nKG. rewrite -(quotientSGK nKC) //; last first. by rewrite /= -pseries1 (pseries_sub_catl [::_]). -apply: subset_trans (quotient_subcent _ _ _) _ ;rewrite /= -/K. +apply: subset_trans (quotient_subcent _ _ _) _; rewrite /= -/K. suffices ->: P / K = 'O_p(G / K). rewrite quotient_pseries2 -Fitting_eq_pcore ?trivg_pcore_quotient // -/K. by rewrite cent_sub_Fitting ?morphim_sol. @@ -753,7 +753,7 @@ apply/andP; split; last by apply/bigcupsP=> B _; apply: subsetIl. have [Z1 | ntZ] := eqsVneq 'Z(G) 1. by rewrite (TI_center_nil _ (normal_refl G)) ?Z1 ?(setIidPr _) ?sub1G. have{ntZ} [M /= minM] := minnormal_exists ntZ (gFnorm_trans _ nGA). -rewrite subsetI centsC => /andP[sMG /cents_norm nMG]. +rewrite subsetI centsC => /andP[sMG /cents_norm nMG]. have coMA := coprimeSg sMG coGA; have{nilG} solG := nilpotent_sol nilG. have [nMA ntM abelM] := minnormal_solvable minM sMG solG. set GC := <<_>>; have sMGC: M \subset GC. @@ -1145,7 +1145,7 @@ apply/idP/idP=> [p1G | pU]. have nOG: 'O_{p^', p}(G) <| G by apply: pseries_normal. rewrite eqEsubset pseries_sub. rewrite -(quotientSGK (normal_norm nOG)) ?(pseries_sub_catl [:: _; _]) //=. -rewrite (quotient_pseries [::_;_]) pcore_max //. +rewrite (quotient_pseries [::_; _]) pcore_max //. rewrite /pgroup card_quotient ?normal_norm //. apply: pnat_dvd (indexgS G (_ : p_elt_gen p G \subset _)) _; last first. case p_pr: (prime p); last by rewrite p'natEpi // mem_primes p_pr. diff --git a/mathcomp/odd_order/BGsection10.v b/mathcomp/odd_order/BGsection10.v index 5a61e25..dbe9c6b 100644 --- a/mathcomp/odd_order/BGsection10.v +++ b/mathcomp/odd_order/BGsection10.v @@ -108,7 +108,7 @@ Lemma MalphaJ x : (H :^ x)`_\alpha = H`_\alpha :^ x. Proof. by rewrite /alpha_core -(eq_pcore H (alphaJ x)) pcoreJ. Qed. Lemma betaJ x : \beta(H :^ x) =i \beta(H). -Proof. +Proof. move=> p; apply/forall_inP/forall_inP=> nnSylH P sylP. by rewrite -(@narrowJ _ _ _ x) nnSylH ?pHallJ2. by rewrite -(@narrowJ _ _ _ x^-1) nnSylH // -(pHallJ2 _ _ _ x) actKV. @@ -136,7 +136,7 @@ Hypothesis maxM : M \in 'M. (* This is the first inclusion in the remark following the preliminary *) (* definitions in B & G, p. 70. *) Remark beta_sub_alpha : {subset \beta(M) <= \alpha(M)}. -Proof. +Proof. move=> p; rewrite !inE /= => /forall_inP nnSylM. have [P sylP] := Sylow_exists p M; have:= nnSylM P sylP. by rewrite negb_imply (p_rank_Sylow sylP) => /andP[]. @@ -221,7 +221,7 @@ Implicit Type A E H K M N P Q R S V W X Y : {group gT}. Theorem sigma_Sylow_trans M p X g : p \in \sigma(M) -> p.-Sylow(M) X -> X :^ g \subset M -> g \in M. Proof. -move=> sMp sylX sXgM; have pX := pHall_pgroup sylX. +move=> sMp sylX sXgM; have pX := pHall_pgroup sylX. have [|h hM /= sXghX] := Sylow_Jsub sylX sXgM; first by rewrite pgroupJ. by rewrite -(groupMr _ hM) (subsetP (norm_sigma_Sylow _ sylX)) ?inE ?conjsgM. Qed. @@ -369,7 +369,7 @@ move=> hallH; have [sHM sH _] := and3P hallH. rewrite -(Sylow_gen H) gen_subG; apply/bigcupsP=> P /SylowP[p p_pr sylP]. have [-> | ntP] := eqsVneq P 1; first by rewrite sub1G. have [sPH pP _] := and3P sylP; have{ntP} [_ p_dv_P _] := pgroup_pdiv pP ntP. -have{p_dv_P} s_p: p \in \sigma(M) := pgroupP (pgroupS sPH sH) p p_pr p_dv_P. +have{p_dv_P} s_p: p \in \sigma(M) := pgroupP (pgroupS sPH sH) p p_pr p_dv_P. have{sylP} sylP: p.-Sylow(M) P := subHall_Sylow hallH s_p sylP. have [sPM nMP] := (pHall_sub sylP, norm_sigma_Sylow s_p sylP). have sylP_G := sigma_Sylow_G maxM s_p sylP. @@ -378,7 +378,7 @@ have defG': G^`(1) = G. by have [?|//] := simpG _ (der_normal 1 _); case/derG1P: (mFT_nonAbelian gT). rewrite -subsetIidl -{1}(setIT P) -defG'. rewrite (focal_subgroup_gen sylP_G) (focal_subgroup_gen sylP) genS //. -apply/subsetP=> _ /imset2P[x g Px /setIdP[Gg Pxg] ->]. +apply/subsetP=> _ /imset2P[x g Px /setIdP[Gg Pxg] ->]. pose X := <[x]>; have sXM : X \subset M by rewrite cycle_subG (subsetP sPM). have sXgM: X :^ g \subset M by rewrite -cycleJ cycle_subG (subsetP sPM). have [trMX _ _] := sigma_group_trans maxM s_p (mem_p_elt pP Px). @@ -399,7 +399,7 @@ Qed. (* This is B & G, Theorem 10.2(b1). *) Theorem Msigma_Hall : \sigma(M).-Hall(M) M`_\sigma. -Proof. +Proof. have [H hallH] := Hall_exists \sigma(M) solM; have [sHM sH _] := and3P hallH. rewrite /M`_\sigma (normal_Hall_pcore hallH) // -(quotientGK nsMaM). rewrite -(quotientGK (normalS _ sHM nsMaM)) ?cosetpre_normal //; last first. @@ -420,7 +420,7 @@ Qed. (* This is B & G, Theorem 10.2(b2). *) Theorem Msigma_Hall_G : \sigma(M).-Hall(G) M`_\sigma. -Proof. +Proof. rewrite pHallE subsetT /= eqn_dvd {1}(card_Hall Msigma_Hall). rewrite partn_dvd ?cardG_gt0 ?cardSg ?subsetT //=. apply/dvdn_partP; rewrite ?part_gt0 // => p. @@ -501,7 +501,7 @@ rewrite leq_eqVlt; case: ltngtP => // rCPB _. have: 2 < 'r('C(B)) by rewrite (leq_trans rCPB) ?rankS ?subsetIr. by apply: cent_rank3_Uniqueness; rewrite -dimB -rank_abelem. have cPX: P \subset 'C(X). - have EpPB: B \in 'E_p(P) by apply/pElemP. + have EpPB: B \in 'E_p(P) by apply/pElemP. have coPX: coprime #|P| #|X| := coprimeSg sPMa coMaX. rewrite centsC (coprime_odd_faithful_cent_abelem EpPB) ?mFT_odd //. rewrite -(setIid 'C(B)) setIA (pmaxElem_LdivP p_pr _) 1?centsC //. @@ -606,7 +606,7 @@ have [P sylP sXP] := Sylow_superset sXM pX; have [sPM pP _] := and3P sylP. pose T := 'Ohm_1('Z(P)); pose A := X <*> T; have nilP := pgroup_nil pP. have charT: T \char P by apply/gFchar_trans/gFchar. have neqTX: T != X. - apply: contraNneq s'p => defX; apply/exists_inP; exists P => //. + apply: contraNneq s'p => defX; apply/exists_inP; exists P => //. by rewrite (subset_trans _ sNXM) // -defX char_norms. have rP: 'r(P) = 2 by rewrite (rank_Sylow sylP) rpM2. have ntT: T != 1 by rewrite Ohm1_eq1 center_nil_eq1 // -rank_gt0 rP. @@ -626,7 +626,7 @@ Qed. End OneMaximal. (* This is B & G, Theorem 10.6. *) -Theorem mFT_proper_plength1 p H : H \proper G -> p.-length_1 H. +Theorem mFT_proper_plength1 p H : H \proper G -> p.-length_1 H. Proof. case/mmax_exists=> M /setIdP[maxM sHM]. suffices{H sHM}: p.-length_1 M by apply: plength1S. @@ -765,7 +765,7 @@ have sQyxP: Q :^ (y * x) \subset P. by rewrite actM (subset_trans _ sRxP) // -(normP nRy) !conjSg. have [t tNP defQx] := mFT_sub_Sylow_trans sQP sQxP. have [z zNP defQxy] := mFT_sub_Sylow_trans sQP sQyxP. -by rewrite inE -(conjSg _ _ x) -actM /= defQx defQxy !(normsP nQ_NP). +by rewrite inE -(conjSg _ _ x) -actM /= defQx defQxy !(normsP nQ_NP). Qed. End OneSylow. @@ -904,7 +904,7 @@ have{nilM'W} nilW: nilpotent W. rewrite -(Lagrange_index (subsetIr _ _) (pcore_sub _ _)) pnat_mul //. rewrite -(divgS (pcore_sub _ _)) -card_quotient ?normsI ?normG //= -pgroupE. rewrite (pi_p'group qWWM') //= -(dprod_card (nilpotent_pcoreC p nilM'W)). - by rewrite mulKn ?cardG_gt0 // -pgroupE pcore_pgroup. + by rewrite mulKn ?cardG_gt0 // -pgroupE pcore_pgroup. have [[sWqW qWq _] [sWpW pWp _]] := (and3P sylWq, and3P sylWp). have <-: Wp * Wq = W. apply/eqP; rewrite eqEcard mul_subG //= -(partnC q (cardG_gt0 W)). @@ -929,7 +929,7 @@ split=> // [a_p | {part1}sylX]. have ltCMX_G := sub_proper_trans (subsetIl M 'C(X)) ltMG. have [P sylP cPX] := part1; have s_p := alpha_sub_sigma maxM a_p. have{sylP} sylP := subHall_Sylow hallMs s_p sylP. - apply: rank3_Uniqueness ltCMX_G (leq_trans a_p _). + apply: rank3_Uniqueness ltCMX_G (leq_trans a_p _). by rewrite -(rank_Sylow sylP) rankS //= subsetI (pHall_sub sylP) // centsC. do [move: sWXM'; rewrite (joing_idPr (pHall_sub sylX)) => sWM'] in hallW. have nMbX: X \subset 'N(M`_\beta) := subset_trans sXM (normal_norm nsMbM). @@ -1151,7 +1151,7 @@ have rZle1: 'r(Z) <= 1. rewrite -(TI_pcoreC \sigma(M) M 'F(M)) subsetI commg_subl commg_subr. by rewrite (subset_trans sZM) ?gFnorm ?gFsub_trans. have{rZle1} cycZ: cyclic Z. - have nilZ: nilpotent Z := nilpotentS (gFsub _ _) Fnil. + have nilZ: nilpotent Z := nilpotentS (gFsub _ _) Fnil. by rewrite nil_Zgroup_cyclic // odd_rank1_Zgroup // mFT_odd. have cZM': M^`(1) \subset 'C_M(Z). rewrite der1_min ?normsI ?normG ?norms_cent //= -ker_conj_aut. @@ -1453,7 +1453,7 @@ case/andP=> /pElemP[_ abelF] ltAF; have [pF cFF _] := and3P abelF. apply: uniq_mmaxS sAR (mFT_pgroup_proper pR) _. have rCAgt2: 'r('C(A)) > 2. rewrite -dimA (leq_trans (properG_ltn_log pF ltAF)) // -(rank_abelem abelF). - by rewrite rankS // centsC (subset_trans (proper_sub ltAF)). + by rewrite rankS // centsC (subset_trans (proper_sub ltAF)). by apply: cent_rank3_Uniqueness rCAgt2; rewrite (rank_abelem abelA) dimA. Qed. diff --git a/mathcomp/odd_order/BGsection11.v b/mathcomp/odd_order/BGsection11.v index fe41e8d..ae376c3 100644 --- a/mathcomp/odd_order/BGsection11.v +++ b/mathcomp/odd_order/BGsection11.v @@ -255,7 +255,7 @@ have [X1 EpX1 nregX11] := nregA _ ntQ1 nQ1A coQ1A. pose Q2 := Q1 :^ g; have sylQ2: q.-Sylow(Ms :^ g) Q2 by rewrite pHallJ2. have{ntQ1} ntQ2: Q2 != 1 by rewrite -!cardG_gt1 cardJg in ntQ1 *. have nQ2A: A \subset 'N(Q2) by rewrite (subset_trans sAP) ?norm_conj_norm. -have{coQ1A} coQ2A: coprime #|Q2| #|A| by rewrite cardJg. +have{coQ1A} coQ2A: coprime #|Q2| #|A| by rewrite cardJg. have{nregA ntQ2 coQ2A} [X2 EpX2 nregX22] := nregA _ ntQ2 nQ2A coQ2A. have [|_ regA]:= exceptional_TIsigmaJ notMg _ sylQ1 nQ1A sylQ2 nQ2A. by rewrite (subset_trans sAP) // -(normP nPg) conjSg. @@ -424,7 +424,7 @@ have qQ0: q.-group Q0 := pgroupS sQ0Q qQ. have p'Q0: p^'.-group Q0 by apply: (pi_pnat qQ0); rewrite eq_sym in q'p. have sM'Q0: \sigma(M)^'.-group Q0 := pi_pnat qQ0 sM'q. have cQ0Q0: abelian Q0 := center_abelian Q. -have defQ0: [~: A, Q0] = Q0. +have defQ0: [~: A, Q0] = Q0. rewrite -{2}[Q0](coprime_abelian_cent_dprod nQ0A) //. by rewrite setIAC regQ setI1g dprodg1 commGC. by rewrite (coprimeSg (subset_trans sQ0Q sQK)). diff --git a/mathcomp/odd_order/BGsection12.v b/mathcomp/odd_order/BGsection12.v index 1dc8454..7cc32ed 100644 --- a/mathcomp/odd_order/BGsection12.v +++ b/mathcomp/odd_order/BGsection12.v @@ -100,7 +100,7 @@ rewrite (solvableS sEM) // mFT_sol // properT. apply: contraNneq (pgroupP s'E p p_pr pE) => ->. have [P sylP] := Sylow_exists p [set: gT]. by apply/exists_inP; exists P; rewrite ?subsetT. -Qed. +Qed. Let solE := sigma_compl_sol. Let exHallE pi := exists Ei : {group gT}, pi.-Hall(E) Ei. @@ -233,7 +233,7 @@ Qed. (* This is B & G, Lemma 12.1(g). *) Lemma tau2_not_beta p : - p \in \tau2(M) -> p \notin \beta(G) /\ {subset 'E_p^2(M) <= 'E*_p(G)}. + p \in \tau2(M) -> p \notin \beta(G) /\ {subset 'E_p^2(M) <= 'E*_p(G)}. Proof. case/andP=> s'p /eqP rpM; split; first exact: sigma'_rank2_beta' rpM. by apply/subsetP; apply: sigma'_rank2_max. @@ -255,7 +255,7 @@ Lemma sigma_compl_context M E E1 E2 E3 : & (*f*) 'C_E3(E) = 1]. Proof. move=> maxM [hallE hallE1 hallE2 hallE3 groupE21]. -have [sEM solM] := (pHall_sub hallE, mmax_sol maxM). +have [sEM solM] := (pHall_sub hallE, mmax_sol maxM). have [[sE1E t1E1 _] [sE3E t3E3 _]] := (and3P hallE1, and3P hallE3). have tiE'E1: E^`(1) :&: E1 = 1. rewrite coprime_TIg // coprime_pi' ?cardG_gt0 //. @@ -308,7 +308,7 @@ have SylowE3 P: Sylow E3 P -> [/\ cyclic P, P \subset E^`(1) & 'C_P(E) = 1]. rewrite -{2}(Frattini_arg nsEp'P_E sylP_Ep'P) /= !norm_joinEr //. by rewrite -mulgA (normC nPK) -mulPK -{1}(mulGid P) !mulgA. have ntPE': P :&: E^`(1) != 1. - have sylPE' := Hall_setI_normal (der_normal 1 E) sylP_E. + have sylPE' := Hall_setI_normal (der_normal 1 E) sylP_E. rewrite -rank_gt0 (rank_Sylow sylPE') p_rank_gt0. by rewrite (tau3E maxM hallE) in t3p; case/andP: t3p. have defP := coprime_abelian_cent_dprod nPK coPK (cyclic_abelian cycP). @@ -379,7 +379,7 @@ Lemma prime_class_mmax_norm M p X : M \in 'M -> p.-group X -> 'N(X) \subset M -> (p \in \sigma(M)) || (p \in \tau2(M)). Proof. -move=> maxM pX sNM; rewrite -implyNb; apply/implyP=> sM'p. +move=> maxM pX sNM; rewrite -implyNb; apply/implyP=> sM'p. by rewrite 3!inE /= sM'p (sigma'_norm_mmax_rank2 _ _ pX). Qed. @@ -462,7 +462,7 @@ have [sHp | sH'p] := boolP (p \in \sigma(H)); last first. rewrite setIC coprime_TIg ?coprime_morph //. rewrite (pnat_coprime (pcore_pgroup _ _)) // (card_pnElem Ep2A). by rewrite pnat_exp ?orbF ?pnatE. - rewrite commg_subI // subsetI ?joing_subr ?subsetIl. + rewrite commg_subI // subsetI ?joing_subr ?subsetIl. by rewrite (subset_trans sAM) ?gFnorm. by rewrite setIC subIset ?nHsA_H. have sAHs: A \subset H`_\sigma. @@ -918,7 +918,7 @@ have defFM: Ms \x A0 = 'F(M). have sNQM: 'N(Q) \subset M. rewrite (mmax_normal maxM) // (nilpotent_Hall_pcore nilF sylQ). by rewrite p_core_Fitting pcore_normal. - apply/implyP; rewrite implyNb /= -def_t2 orbC. + apply/implyP; rewrite implyNb /= -def_t2 orbC. by rewrite (prime_class_mmax_norm maxM qQ). rewrite pcore_max ?(pi_p'group (pcore_pgroup _ _)) //. rewrite [_ <| _]andbC gFsub_trans ?gFnorm //. @@ -1414,7 +1414,7 @@ have{sE3E} sK_CEA: K \subset 'C_E(A). by rewrite (subset_trans _ sAE2) // commg_subr (subset_trans sE3E). split=> // [_ F2 F3 [_ _ hallF2 hallF3 _] | ]. have solE: solvable E := solvableS sEM (mmax_sol maxM). - have [x2 Ex2 ->] := Hall_trans solE hallF2 hallE2. + have [x2 Ex2 ->] := Hall_trans solE hallF2 hallE2. have [x3 Ex3 ->] := Hall_trans solE hallF3 hallE3. rewrite mulG_subG !sub_conjg !(normsP (normal_norm nsCAE)) ?groupV //. by rewrite -mulG_subG mulE32. @@ -1597,7 +1597,7 @@ have t2Lq: q \in \tau2(L). have /orP[sLq | //] := prime_class_mmax_norm maxL qQ0 sNQ0_L. by have /orP[/andP[/negP] | ] := pnatPpi (part_b L maxNA_L) piCEAb_q. have [cQQ [/= sL'q _]] := (cyclic_abelian cycQ, andP t2Lq). -have sQL: Q \subset L := subset_trans (centsS sQ0Q cQQ) sCQ0_L. +have sQL: Q \subset L := subset_trans (centsS sQ0Q cQQ) sCQ0_L. have [F hallF sQF] := Hall_superset (mmax_sol maxL) sQL (pi_pnat qQ sL'q). have [B Eq2B _] := ex_tau2Elem hallF t2Lq. have [_ sLp]: _ /\ p \in \sigma(L) := andP (part_a L maxNA_L p t2Mp). @@ -1703,11 +1703,11 @@ have [cSS | not_cSS] := boolP (abelian S); last first. by rewrite ltnS logn_gt0. have defM0: Ms ><| U0 = Ms <*> U0 := sdprod_subr defMsU (subsetIr _ _). have frobM0: [Frobenius Ms <*> U0 = Ms ><| U0]. - apply/Frobenius_semiregularP=> // [|e /setD1P[nte /setIP[E0e Ue]]]. - by rewrite -rank_gt0 (leq_trans _ (p_rank_le_rank p _)) ?p_rank_gt0. + apply/Frobenius_semiregularP=> // [|e /setD1P[nte /setIP[E0e Ue]]]. + by rewrite -rank_gt0 (leq_trans _ (p_rank_le_rank p _)) ?p_rank_gt0. have [ | ] := boolP (p13.-elt e); first by apply: regU13; rewrite !inE nte. apply: contraNeq => /trivgPn[x /setIP[Ms_x cex] ntx]. - apply/pgroupP=> q q_pr q_dv_x ; rewrite inE /= (regE0 x) ?inE ?ntx //. + apply/pgroupP=> q q_pr q_dv_x; rewrite inE /= (regE0 x) ?inE ?ntx //. rewrite mem_primes q_pr cardG_gt0 (dvdn_trans q_dv_x) ?order_dvdG //. by rewrite inE E0e cent1C. have [nsA0U sU0U _ _ _] := sdprod_context defU. @@ -1887,7 +1887,7 @@ have [cSU | not_cSU] := boolP (U \subset 'C(S)). have ntz: <[z]> != 1 by rewrite trivg_card1 -orderE oz -dvdn1 -trivg_exponent. rewrite regNNS ?cycle_cyclic ?cycle_subG //=. suffices /eqP->: 'Ohm_1(<[z]>) == Sn by apply: char_norms; apply: gFchar. - have [p_z pS1] := (mem_p_elt pS Sz, pgroupS (Ohm_sub 1 S) pS). + have [p_z pS1] := (mem_p_elt pS Sz, pgroupS (Ohm_sub 1 S) pS). rewrite eqEcard (Ohm1_cyclic_pgroup_prime _ p_z) ?cycle_cyclic //. rewrite (Ohm_p_cycle _ p_z) oz -/n subn1 cycle_subG Mho_p_elt //=. rewrite (card_pgroup (pgroupS sSnS1 pS1)) (leq_exp2l _ 1) ?prime_gt1 //. @@ -1969,7 +1969,7 @@ have [X]: exists2 X, X \in subgroups Q & ('C_S(X) != 1) && ([~: S, X] != 1). have ltNA_G: 'N(A) \proper G. by rewrite defNS mFT_norm_proper // (mFT_pgroup_proper pS). have [H maxNA_H] := mmax_exists ltNA_G. - have nCEA_Q1 := subset_trans sQ1E (normal_norm nsCEA). + have nCEA_Q1 := subset_trans sQ1E (normal_norm nsCEA). have [_ _] := primes_norm_tau2Elem maxM hallE t2p Ep2A maxNA_H. case/(_ q)=> [||t2Hq [S2 sylS2 nsS2H] _]. - rewrite -p_rank_gt0 -(rank_Sylow (quotient_pHall _ sylQ1)) //. @@ -2371,7 +2371,7 @@ without loss sXMs: M maxM sM_Y sMq / X \subset M`_\sigma. have [x Gx sXQx] := Sylow_subJ sylQ_G (subsetT X) qX. have: X \subset M`_\sigma :^ x by rewrite (subset_trans sXQx) ?conjSg. rewrite -MsigmaJ => /IH; rewrite sigmaJ mmaxJ (eq_pgroup _ (sigmaJ _ _)). - case => // [[y sYyMx] parts_ab]. + case=> // [[y sYyMx] parts_ab]. split=> [|E p H hallE piEp bG'p maxY_H notMGH]. by exists (y * x^-1); rewrite conjsgM sub_conjgV -MsigmaJ. have:= parts_ab (E :^ x)%G p H; rewrite tau1J /= cardJg pHallJ2. diff --git a/mathcomp/odd_order/BGsection13.v b/mathcomp/odd_order/BGsection13.v index e90be7f..de9ddaf 100644 --- a/mathcomp/odd_order/BGsection13.v +++ b/mathcomp/odd_order/BGsection13.v @@ -95,7 +95,7 @@ have sSH': S \subset H^`(1). have [[F1 hallF1] [F3 hallF3]] := ex_tau13_compl hallF. have [F2 _ complFi] := ex_tau2_compl hallF hallF1 hallF3. have [[sF3F' nsF3F] _ _ _ _] := sigma_compl_context maxH complFi. - apply: subset_trans (subset_trans sF3F' (dergS 1 (pHall_sub hallF))). + apply: subset_trans (subset_trans sF3F' (dergS 1 (pHall_sub hallF))). by rewrite (sub_normal_Hall hallF3) ?(pi_pgroup pS). have sylS_H' := pHall_subl sSH' (der_sub 1 H) sylS. split=> // [P sPMH pP | t1Mp]; last first. @@ -246,7 +246,7 @@ without loss symPR: p r P R EpP ErR cPR t1Mp / rewrite sCaPR -(setIidPl sMaMs) -!setIA setIS ?(IH r p) 1?centsC // => _. by case/eqVproper; rewrite // /proper sCaPR andbF. do [rewrite !subsetI !subsetIl /=; set cRCaP := _ \subset _] in symPR *. -pose Mz := 'O_(if cRCaP then \sigma(M) else \alpha(M))(M); pose C := 'C_Mz(P). +pose Mz := 'O_(if cRCaP then \sigma(M) else \alpha(M))(M); pose C := 'C_Mz(P). suffices: C \subset 'C(R) by rewrite /C /Mz /cRCaP; case: ifP => // ->. have sMzMs: Mz \subset Ms by rewrite /Mz; case: ifP => // _. have sCMs: C \subset Ms by rewrite subIset ?sMzMs. @@ -276,7 +276,7 @@ have [sPH sRH] := (subset_trans cPP sCPH, subset_trans cPR sCPH). have [sSM sSH] := (subset_trans sSMs sMsM, subset_trans cPS sCPH). have [sQM sQH] := (subset_trans sQS sSM, subset_trans sQS sSH). have ntMsH_R: [~: Ms :&: H, R] != 1. - by rewrite (subG1_contra _ ntQ) ?commSg // subsetI sSMs. + by rewrite (subG1_contra _ ntQ) ?commSg // subsetI sSMs. have sR_EH: R \subset E :&: H by apply/subsetIP. have ntMsH_MH: [~: Ms :&: H, M :&: H] != 1. by rewrite (subG1_contra _ ntMsH_R) ?commgS // (subset_trans sR_EH) ?setSI. @@ -308,7 +308,7 @@ have ntHa: H`_\alpha != 1 by rewrite (subG1_contra _ ntCHaRQ) ?subsetIl. have uniqNQ: 'M('N(Q)) = [set H]. apply: contraNeq ntCHaRQ; rewrite joingC. by case/(cent_Malpha_reg_tau1 _ _ r'q ErH_R) => //; case=> //= _ -> _. -have maxNQ_H: H \in 'M('N(Q)) :\ M by rewrite uniqNQ !inE neqHM /=. +have maxNQ_H: H \in 'M('N(Q)) :\ M by rewrite uniqNQ !inE neqHM /=. have{maxNQ_H} [_ _] := sigma_subgroup_embedding maxM sMq sQM qQ ntQ maxNQ_H. have [sHq [_ st1HM [_ ntMa]] | _ [_ _ sM'MH]] := ifP; last first. have piPp: p \in \pi(P) by rewrite -p_rank_gt0 p_rank_abelem ?dimP. @@ -590,7 +590,7 @@ move=> [maxM maxL notMGL] [t1Mp t1Lp EpP] [sylQ sylU nQP nUP]. move=> [regPQ regPU] [sNQL sNUM]; rewrite setIC in sylU. (* for symmetry *) have notLGM: gval M \notin L :^: G by rewrite orbit_sym. (* for symmetry *) have{EpP} [ntP [sPML abelP dimP]] := (nt_pnElem EpP isT, pnElemP EpP). -have{sPML} [[sPM sPL] [pP _ _]] := (subsetIP sPML, and3P abelP). +have{sPML} [[sPM sPL] [pP _ _]] := (subsetIP sPML, and3P abelP). have solCP: solvable 'C(P) by rewrite mFT_sol ?mFT_cent_proper. pose Qprops M q Q := [&& q.-Sylow(M) Q, q != p, q \notin \beta(M), 'C_(M`_\beta)(P) != 1 & 'C_(M`_\beta)(P <*> Q) == 1]. @@ -662,7 +662,7 @@ have{ntX} sHM: H \subset M. by rewrite beta_norm_sub_mmax // /psubgroup (subset_trans sYMb). have [_ trCY _] := sigma_group_trans maxM (beta_sub_sigma maxM bMt) tY. have [|| h cYh /= defMg] := (atransP2 trCY) M (M :^ g). - - by rewrite inE orbit_refl (subset_trans (normG _) sNY_M). + - by rewrite inE orbit_refl (subset_trans (normG _) sNY_M). - by rewrite inE mem_orbit ?in_setT. by rewrite defMg conjGid // (subsetP sNY_M) ?(subsetP (cent_sub _)) in sHMg. have sXMb: X \subset M`_\beta. @@ -743,7 +743,7 @@ have{not_pM'} [R ErR nQR]: exists2 R, R \in 'E_r^1('C_M(P)) & R \subset 'N(Q). have [T [sylT nTP sRT]] := coprime_Hall_subset nKP coKP solK sRK rR nRP. have [x cKPx defS] := coprime_Hall_trans nKP coKP solK sylS_K nSP sylT nTP. rewrite -(conjGid (subsetP (setSI _ sKM) x cKPx)). - by exists (R :^ x)%G; rewrite ?pnElemJ ?(subset_trans _ nQS) // defS conjSg. + by exists (R :^ x)%G; rewrite ?pnElemJ ?(subset_trans _ nQS) // defS conjSg. have [sRcMP abelR _] := pnElemP ErR; have ntR := nt_pnElem ErR isT. have{sRcMP abelR} [[sRM cPR] [rR _]] := (subsetIP sRcMP, andP abelR). have sNR_L: 'N(R) \subset L. @@ -957,7 +957,7 @@ have{hallE2} E2_1: E2 :==: 1. apply/idPn; rewrite -rank_gt0; have [p _ ->] := rank_witness E2. rewrite p_rank_gt0 => /(pnatPpi (pHall_pgroup hallE2))t2p. have [A Ep2A _] := ex_tau2Elem hallE t2p. - by apply: not_regE3Ms; case: (tau2_regular maxM complEi t2p Ep2A). + by apply: not_regE3Ms; case: (tau2_regular maxM complEi t2p Ep2A). have [_ ntE1 [cycE1 cycE3] [defE _] _] := sigma_compl_context maxM complEi. rewrite (eqP E2_1) sdprod1g in defE; have{ntE1} ntE1 := ntE1 E2_1. have [nsE3E _ mulE31 nE31 _] := sdprod_context defE. @@ -977,7 +977,7 @@ have [p Ep1X] := nElemP EpX; have [sXE abelX oX] := pnElemPcard Ep1X. have [p_pr ntX] := (pnElem_prime Ep1X, nt_pnElem Ep1X isT). have tau31p: p \in [predU \tau3(M) & \tau1(M)]. rewrite (pgroupP (pgroupS sXE _)) ?oX // -mulE31 pgroupM. - rewrite (sub_pgroup _ t3E3) => [|q t3q]; last by rewrite inE /= t3q. + rewrite (sub_pgroup _ t3E3) => [|q t3q]; last by rewrite inE /= t3q. by rewrite (sub_pgroup _ t1E1) // => q t1q; rewrite inE /= t1q orbT. have [/= t3p | t1p] := orP tau31p. rewrite (char_normal_trans _ nsE3E) ?sub_cyclic_char //. @@ -1028,7 +1028,7 @@ have [sLq t12Lp]: q \in \sigma(L) /\ (p \in \tau1(L)) || (p \in \tau2(L)). rewrite -subG1 quotient_sub1 ?subsetI ?sPE // (subset_trans sPE) //. by rewrite normsI ?normG ?norms_cent. have [maxL sNL] := setIdP maxNL; have sEL := subset_trans nAE sNL. -have sL'p: p \in \sigma(L)^' by move: t12Lp; rewrite -andb_orr => /andP[]. +have sL'p: p \in \sigma(L)^' by move: t12Lp; rewrite -andb_orr => /andP[]. have [sPL sL'P] := (subset_trans sPE sEL, pi_pgroup pP sL'p). have{sL'P} [F hallF sPF] := Hall_superset (mmax_sol maxL) sPL sL'P. have solF := sigma_compl_sol hallF. diff --git a/mathcomp/odd_order/BGsection14.v b/mathcomp/odd_order/BGsection14.v index 2e3f523..bc6f9e2 100644 --- a/mathcomp/odd_order/BGsection14.v +++ b/mathcomp/odd_order/BGsection14.v @@ -400,16 +400,16 @@ by apply: sub_in_pnat => p /(pnatPpi skM)/orP[] // kMp /negP. Qed. Lemma FtypeJ M x : ((M :^ x)%G \in 'M_'F) = (M \in 'M_'F). -Proof. by rewrite inE mmaxJ pgroupJ (eq_p'group _ (kappaJ M x)) !inE. Qed. +Proof. by rewrite inE mmaxJ pgroupJ (eq_p'group _ (kappaJ M x)) !inE. Qed. Lemma PtypeJ M x : ((M :^ x)%G \in 'M_'P) = (M \in 'M_'P). -Proof. by rewrite !in_setD mmaxJ FtypeJ. Qed. +Proof. by rewrite !in_setD mmaxJ FtypeJ. Qed. Lemma P1typeJ M x : ((M :^ x)%G \in 'M_'P1) = (M \in 'M_'P1). Proof. rewrite inE PtypeJ pgroupJ [M \in 'M_'P1]inE; congr (_ && _). by apply: eq_pgroup => p; rewrite inE /= kappaJ sigmaJ. -Qed. +Qed. Lemma P2typeJ M x : ((M :^ x)%G \in 'M_'P2) = (M \in 'M_'P2). Proof. by rewrite in_setD PtypeJ P1typeJ -in_setD. Qed. @@ -529,7 +529,7 @@ have [have_a nK1K ntE1 sE1K]: [/\ part_a, b1_hyp, E1 :!=: 1 & E1 \subset K]. apply: contraNeq (kappa_nonregular (pnatPpi kK piKp) EpMY). move/(subG1_contra (setIS U (centS sYy))). have{y sYy Ky} sYE1 := subset_trans sYy (subset_trans Ky sKE1). - have ntY: Y :!=: 1 by apply: (nt_pnElem EpY). + have ntY: Y :!=: 1 by apply: (nt_pnElem EpY). rewrite -subG1 /=; have [_ <- _ tiE32] := sdprodP defU. rewrite -subcent_TImulg ?subsetI ?(subset_trans sYE1) // mulG_subG. rewrite !subG1 /= => /nandP[nregE3Y | nregE2Y]. @@ -769,7 +769,7 @@ have hallE: \sigma(M)^'.-Hall(M) E. rewrite pHallE /= -/E -mulUK mul_subG //= TI_cardMg //. rewrite -(partnC \kappa(M) (part_gt0 _ _)) (partn_part _ (@kappa_sigma' M)). apply/eqP; rewrite -partnI -(card_Hall hallK) mulnC; congr (_ * _)%N. - by rewrite (card_Hall hallU); apply: eq_partn => p; apply: negb_or. + by rewrite (card_Hall hallU); apply: eq_partn => p; apply: negb_or. have [K1 | ntK] := altP (K :=P: 1). rewrite K1 sdprodg1 -{1}(mulg1 U) -{1}K1 mulUK sdprod_sigma //. by split=> //; first apply: semiregular_prime; apply: semiregular1r. @@ -1448,7 +1448,7 @@ have{K_spec} defZX: {in MX, forall Mi, K_ Mi \x Ks_ Mi = Z}. by rewrite -defNXs (subset_trans sXK) // (subset_trans (joing_subl _ Ks)). have{hallK_Zi} hallK_Z: {in MX, forall Mi, co_sHallK Mi Z}. by move=> Mi MXi; rewrite -(defZX _ MXi); apply: hallK_Zi. -have nsK_Z: {in MX, forall Mi, K_ Mi <| Z /\ Ks_ Mi <| Z}. +have nsK_Z: {in MX, forall Mi, K_ Mi <| Z /\ Ks_ Mi <| Z}. by move=> Mi /defZX; apply: dprod_normal2. have tiKs: {in MX &, forall Mi Mj, gval Mi != gval Mj -> Ks_ Mi :&: Ks_ Mj = 1}. move=> Mi Mj MXi MXj; apply: contraNeq; rewrite -rank_gt0. @@ -1514,7 +1514,7 @@ have defT: \bigcup_(Mi in MX) (Ks_ Mi)^# * (K_ Mi)^# = T. have [sXx abelX dimX] := pnElemP EpX. have piXp: p \in \pi(X) by rewrite -p_rank_gt0 p_rank_abelem ?dimX. have sXK: X \subset K by rewrite (subset_trans sXx) ?cycle_subG. - have E1X: X \in 'E^1(K) by apply/nElemP; exists p; apply/pnElemP. + have E1X: X \in 'E^1(K) by apply/nElemP; exists p; apply/pnElemP. have [Mi MNXi sXMis] := exMNX X E1X; have MXi: Mi \in MX := setU1r M MNXi. have sXZ: X \subset Z := subset_trans sXK (joing_subl _ _). have sMip: p \in \sigma(Mi) := pnatPpi (pcore_pgroup _ _) (piSg sXMis piXp). @@ -1609,9 +1609,9 @@ have oTG: (#|TG|%:R = (1 + n / z - \sum_(Mi in MX) (k_ Mi)^-1) * g)%R. rewrite natrM natf_indexg ?subsetT //= -/z -mulrA mulrC; congr (_ * _)%R. rewrite oT natrB; last by rewrite ltnW // -subn_gt0 lt0n -oT cards_eq0. rewrite mulrC natrD -/n -/z natr_sum /=. - rewrite mulrBl mulrDl big_distrl divff //=; congr (_ - _)%R. + rewrite mulrBl mulrDl big_distrl divff //=; congr (_ - _)%R. apply: eq_bigr => Mi MXi; have defZi := defZX _ MXi. - by rewrite /z -(dprod_card defZi) natrM invfM mulrC divfK. + by rewrite /z -(dprod_card defZi) natrM invfM mulrC divfK. have neMNX: MNX != set0. move: ntK; rewrite -rank_gt0 => /rank_geP[X /exMNX[Mi MNXi _]]. by apply/set0Pn; exists Mi. @@ -1722,7 +1722,7 @@ have{nilMis} cycZ: cyclic Z. apply: wlog_neg; rewrite -ltnNge ltn_neqAle p_rank_gt0 => /andP[_ piSp]. have [_ /and3P[sKjMj kKj _]] := PmaxMX _ MXj. rewrite -(rank_kappa (pnatPpi kKj (piSg sSKj piSp))) p_rankS //. - exact: subset_trans sSKj sKjMj. + exact: subset_trans sSKj sKjMj. rewrite (dprod_nil (defZX _ MXi)) abelian_nil ?cyclic_abelian //=. exact: (nilpotentS (subsetIl _ _)) nilMis. have cycK: cyclic K := cyclicS (joing_subl _ _) cycZ. @@ -1798,7 +1798,7 @@ have oTGgt_g2: (g / 2%:R < #|TG|%:R)%R. without loss [lt1p ltpq]: p q odd_p odd_q / 1 < p /\ p < q. have [p_pr q_pr]: prime p /\ prime q by rewrite !pdiv_prime ?cardG_gt1. have [ltpq | ltqp | eqpq] := ltngtP p q. - - by apply; rewrite ?prime_gt1. + - by apply; rewrite ?prime_gt1. - by rewrite mulrC; apply; rewrite ?prime_gt1. have [] := hallK_Z _ MX0. rewrite K0 Ks0 => /and3P[_ sM'K _] /and3P[_ sMKs _]. @@ -1839,7 +1839,7 @@ rewrite defZhat {1}defKs; split; first 2 [by split]. rewrite sub_abelian_cent ?cyclic_abelian //=; last first. by rewrite (subset_trans sxK) ?joing_subl. move: ntx; rewrite -rank_gt0 /= -{1}(setIidPr sxK) => /rank_geP[X]. - rewrite nElemI -setIdE -defZ => /setIdP[E1X sXx]. + rewrite nElemI -setIdE -defZ => /setIdP[E1X sXx]. by have [<- _] := defNX _ E1X; rewrite setIS ?cents_norm ?centS. + case/setD1P; rewrite -cycle_eq1 -cycle_subG -cent_cycle => nty syKs. have [_ [defNKs defNY] _ _ _] := Ptype_structure PmaxMstar hallKstar. @@ -2067,7 +2067,7 @@ have [Mst _ [_ _ _ [cycZ _ defZ _ _] _]] := Ptype_embedding PmaxM hallK. rewrite -(mulKVg y x) -/y' 2!inE negb_or andbC. do [set Ks := 'C_(_)(K); set Z := K <*> _] in cycZ defZ *. have Ks_y: y \in Ks. - have cKZ := sub_abelian_cent (cyclic_abelian cycZ) (joing_subl K Ks). + have cKZ := sub_abelian_cent (cyclic_abelian cycZ) (joing_subl K Ks). rewrite inE Ms_y (subsetP cKZ) // -(defZ y'); last by rewrite !inE nty'. by rewrite inE cent1C (subsetP sMsM). have [_ [defNK _] _ _ _] := Ptype_structure PmaxM hallK. @@ -2169,7 +2169,7 @@ have [sKM s'K] := (subset_trans sKE sEM, pgroupS sKE s'E). have regQ: 'C_(M`_\sigma)(Q) = 1. apply/eqP; apply: contraFT (k'M q) => nregQ. have EqQ_M: Q \in 'E_q^1(M) by apply/pnElemP. - by rewrite unlock 3!inE /= t1Mq; apply/exists_inP; exists Q. + by rewrite unlock 3!inE /= t1Mq; apply/exists_inP; exists Q. have nsKM: K <| M. have [s'q _] := andP t1Mq. have EqQ_NK: Q \in 'E_q^1('N_M(K)) by apply/pnElemP; rewrite subsetI sQM. @@ -2240,7 +2240,7 @@ have{t12Hq} [/= t1Hq | /= t2Hq] := orP t12Hq. by have [_ _ _ _ [|<- //]] := Ptype_structure PmaxH hallL; apply/setDP. left; split=> //. have [x defQ]: exists x, Q :=: <[x]> by apply/cyclicP; rewrite prime_cyclic ?oQ. -rewrite defQ cent_cycle in nregQHs *; rewrite (cent1_nreg_sigma_uniq maxH) //. +rewrite defQ cent_cycle in nregQHs *; rewrite (cent1_nreg_sigma_uniq maxH) //. by rewrite 2!inE -cycle_eq1 -cycle_subG -defQ (nt_pnElem EqQ). by rewrite /p_elt /order -defQ oQ pnatE. Qed. @@ -2351,7 +2351,7 @@ have sUHs: U \subset H`_\sigma. have sK_HsDq: K \subset HsDq. rewrite sub_gen ?subsetU // orbC -p_core_Fitting. by rewrite (sub_Hall_pcore (nilpotent_pcore_Hall _ (Fitting_nil _))) ?qK. - have [|sHsDq_H nHsDq_H] := andP (_ : HsDq <| H). + have [|sHsDq_H nHsDq_H] := andP (_ : HsDq <| H). rewrite -(quotientGK nsHsH) -[HsDq]quotientYK //= cosetpre_normal //. by rewrite -{3}mulHsD quotientMidl quotient_normal // pcore_normal. have sU_HsDq: U \subset HsDq. @@ -2458,7 +2458,7 @@ have{p pi_p sMp t2Np b'Mp} FmaxM: M \in 'M_'F. have kMq: q \in \kappa(M). by case/orP: (pnatPpi skM piMq) => //= sMq; case/negP: sM'q. have [K hallK sQK] := Hall_superset (mmax_sol maxM) sQM (pi_pnat qQ kMq). - have EqKQ: Q \in 'E_q^1(K) by apply/pnElemP. + have EqKQ: Q \in 'E_q^1(K) by apply/pnElemP. have [L _ [uniqL [kLhallKs sMhallKs] _ _ _]] := Ptype_embedding PmaxM hallK. set Ks := 'C_(_)(K) in kLhallKs sMhallKs. have{uniqL} defL: 'N[x] :^ g = L. diff --git a/mathcomp/odd_order/BGsection15.v b/mathcomp/odd_order/BGsection15.v index 06d7eb9..704e98d 100644 --- a/mathcomp/odd_order/BGsection15.v +++ b/mathcomp/odd_order/BGsection15.v @@ -242,7 +242,7 @@ set part_c := forall U, _; have c_holds: part_c. have piCx_hyp: {in X^#, forall x', x' \in ('C_M[x])^# /\ \sigma(M)^'.-elt x'}. move=> x' /setD1P[ntx' Xx']; have Ex' := subsetP sXE x' Xx'. rewrite 3!inE ntx' (subsetP sEM) ?(mem_p_elt s'M_E) //=. - by rewrite (subsetP _ _ Xx') ?sub_cent1. + by rewrite (subsetP _ _ Xx') ?sub_cent1. have piCx x' X1x' := (* GG -- ssreflect evar generalization fails in trunk *) let: conj c e := piCx_hyp x' X1x' in pi_of_cent_sigma maxM Ms1x c e. have t2X: \tau2(M).-group X. @@ -250,7 +250,7 @@ set part_c := forall U, _; have c_holds: part_c. have X1x': x' \in X^# by rewrite !inE Xx' -order_gt1 ox' prime_gt1. have [[]|[]] := piCx _ X1x'; last by rewrite /p_elt ox' pnatE. case/idPn; have:= mem_p_elt (pgroupS sXU sk'U) Xx'. - by rewrite /p_elt ox' !pnatE // => /norP[]. + by rewrite /p_elt ox' !pnatE // => /norP[]. suffices cycX: cyclic X. split=> //; have [x' defX] := cyclicP cycX. have X1x': x' \in X^# by rewrite !inE -cycle_eq1 -cycle_subG -defX ntX /=. @@ -292,7 +292,7 @@ have{cycZ cUU} [cycK cUU] := (cyclicS (joing_subl _ _) cycZ, cUU ntK). split=> // [_||/UtypeF[] //]; first split=> //. apply/eqP; rewrite eq_sym eqEcard -(leq_pmul2r (cardG_gt0 K)). have [nsMsU_M _ mulMsU _ _] := sdprod_context defM. - rewrite (sdprod_card defM) (sdprod_card defM') der1_min ?normal_norm //=. + rewrite (sdprod_card defM) (sdprod_card defM') der1_min ?normal_norm //=. by rewrite -(isog_abelian (sdprod_isog defM)) cyclic_abelian. by apply: abelianS cUU; rewrite gen_subG -big_distrr subsetIl. Qed. @@ -348,7 +348,7 @@ have ltM'M: M' \proper M by rewrite (sol_der1_proper solM) ?mmax_neq1. have sMsM': Ms \subset M' := Msigma_der1 maxM. have [-> | ltMF_Ms] := eqVproper sMF_Ms; first by rewrite eqxx Msigma_neq1. set KDpart := (X in _ /\ X); suffices KD_holds: KDpart. - do 2!split=> //; have [K hallK] := Hall_exists \kappa(M) solM. + do 2!split=> //; have [K hallK] := Hall_exists \kappa(M) solM. pose q := #|'C_(M`_\sigma)(K)|; have [D hallD] := Hall_exists q^' solMs. have [_ [_ _ piMFq _] _ _ _] := KD_holds K D hallK (proper_neq ltMF_Ms) hallD. by rewrite -rank_gt0 (leq_trans _ (p_rank_le_rank q _)) ?p_rank_gt0. @@ -467,7 +467,7 @@ have{K1 sK1M sK1K coMsK1 coQK1 prK1 defCMsK1 nQK1 solMs} Qi_rec Qi: rewrite -(setIidPr sLD_Ms) setIAC defCMsK1 quotientS1 //= -/Ks joingC. rewrite norm_joinEl // -(setIidPl sKsQ) -setIA -group_modr // tiQD mul1g. have [-> | ntLKs] := eqVneq (Ks :&: L) 1; first exact: sub1G. - by rewrite subIset ?(implyP regLK) // prime_meetG. + by rewrite subIset ?(implyP regLK) // prime_meetG. apply: (prime_Frobenius_sol_kernel_nil defLK1b). by apply: solvableS (quotient_sol _ solM); rewrite join_subG !quotientS. by rewrite -(card_isog (quotient_isog _ _)) ?coprime_TIg // (coprimeSg sQiQ). @@ -566,7 +566,7 @@ have{frobDKb regQbDb} [p_pr oQb cQbD']: transitivity ('C_Q[x] / Q0); last first. rewrite -(coprime_quotient_cent (subsetIl Q _) nQ0K coQK solQ) /= -/Q0. by rewrite -/Q -(setIidPl sQMs) -!setIA prMsK // !inE ntx. - rewrite -!cent_cycle -quotient_cycle //; rewrite -!cycle_subG in Kx nQ0x. + rewrite -!cent_cycle -quotient_cycle //; rewrite -!cycle_subG in Kx nQ0x. by rewrite coprime_quotient_cent ?(coprimegS Kx). have:= Frobenius_primact frobDKb _ _ _ ntQb _ prQbK regQbDb. have [nQDK solDK] := (subset_trans sDKM nQM, solvableS sDKM solM). @@ -577,7 +577,7 @@ have{cQbD'} sM''FM: M'' \subset 'F(M). have nQMs := subset_trans sMsM nQM. rewrite [M'']dergSn -/M' -defMs -(quotientSGK _ sQFM) ?comm_subG //. rewrite (quotient_der 1) //= -/Ms -mulQD quotientMidl -quotient_der //= -/Q. - by rewrite quotientS // -defFM subsetI sub_astabQ !comm_subG ?quotient_der. + by rewrite quotientS // -defFM subsetI sub_astabQ !comm_subG ?quotient_der. have sQ0Ms := subset_trans sQ0Q sQMs. have ->: 'C_Ms(Ks / Q0 | 'Q) = 'F(M). have sFMcKsb: 'F(M) \subset 'C_Ms(Ks / Q0 | 'Q). @@ -1048,7 +1048,7 @@ split=> // [E E1 E2 E3 complEi | {Y t2Y defF sM'F}]. have E3_1: E3 :=: 1. have [sEM s'E _] := and3P hallE; have sE'M' := dergS 1 sEM. have sE3F: E3 \subset 'F(M) := subset_trans sE3E' (subset_trans sE'M' sM'F). - rewrite -(setIidPr sE3F) coprime_TIg // -(dprod_card defF) coprime_mull. + rewrite -(setIidPr sE3F) coprime_TIg // -(dprod_card defF) coprime_mull. rewrite (pnat_coprime (pcore_pgroup _ _) (pgroupS sE3E s'E)). exact: p'nat_coprime (sub_pgroup (@tau3'2 _ M) t2Y) t3E3. have{defE} defE: E2 ><| E1 = E by rewrite -defE E3_1 sdprod1g. @@ -1106,7 +1106,7 @@ have max_rB A: p.-abelem A -> B \subset A -> 'r_p(A) <= 2. have [x1 defX1]: exists x1, X1 :=: <[x1]>. by apply/cyclicP; rewrite prime_cyclic ?oX1. have Px1: x1 \in P by rewrite -cycle_subG -defX1. - have Px1a: x1 ^ a \in P. + have Px1a: x1 ^ a \in P. by rewrite (subsetP sAaP) // memJ_conjg -cycle_subG -defX1. have [b nPb def_xb] := sigma_Hall_tame maxM sylP_Ms Px1 Px1a. exists (a * b^-1); rewrite !inE !actM !sub_conjgV defX1 /= -!cycleJ def_xb. @@ -1268,7 +1268,7 @@ Theorem tau2_P2type_signalizer M Mstar U K r R H (q := #|K|) : [/\ prime q, \tau2(H) =i (q : nat_pred) & \tau2(M)^'.-group M]. Proof. move: Mstar => L P2maxM complU maxCK_L sylR maxNR_H not_t2'H. -have [[PmaxM notP1maxM] [hallU hallK _]] := (setDP P2maxM, complU). +have [[PmaxM notP1maxM] [hallU hallK _]] := (setDP P2maxM, complU). have q_pr: prime q by have [_ _ _ _ []] := Ptype_structure PmaxM hallK. have [[maxH _] [maxM _]] := (setIdP maxNR_H, setDP PmaxM). have [maxL sCKL] := setIdP maxCK_L; have hallLs := Msigma_Hall maxL. diff --git a/mathcomp/odd_order/BGsection16.v b/mathcomp/odd_order/BGsection16.v index 737a92d..ca73c4b 100644 --- a/mathcomp/odd_order/BGsection16.v +++ b/mathcomp/odd_order/BGsection16.v @@ -267,7 +267,7 @@ Proof. by rewrite (trivg_kappa maxM); case: complU. Qed. Remark trivgPmax : (M \in 'M_'P) = (K :!=: 1). Proof. by rewrite inE trivgFmax maxM andbT. Qed. -Remark FmaxP : reflect (K :==: 1 /\ U :!=: 1) (M \in 'M_'F). +Remark FmaxP : reflect (K :==: 1 /\ U :!=: 1) (M \in 'M_'F). Proof. rewrite (trivg_kappa_compl maxM complU) 2!inE. have [_ hallK _] := complU; rewrite (trivg_kappa maxM hallK). @@ -415,7 +415,7 @@ by rewrite injm_abelian /= ?im_quotient // injm_quotm ?injm_conj. Qed. Lemma FTcoreJ M x : (M :^ x)`_\s = M`_\s :^ x. -Proof. by rewrite /FTcore FTtypeJ FcoreJ derJ; case: ifP. Qed. +Proof. by rewrite /FTcore FTtypeJ FcoreJ derJ; case: ifP. Qed. Lemma FTsupp1J M x : 'A1(M :^ x) = 'A1(M) :^ x. Proof. by rewrite conjD1g -FTcoreJ. Qed. @@ -1073,7 +1073,7 @@ have [K1 | ntK] := eqsVneq K 1. have FmaxM: M \in 'M_'F by rewrite -(trivg_kappa maxM hallK) K1. have ->: FTtype M = 1%N by apply/eqP; rewrite -FTtype_Fmax. have ntU: U :!=: 1 by case/(FmaxP maxM complU): FmaxM. - have defH: H = Ms. + have defH: H = Ms. by apply/Fcore_eq_Msigma; rewrite // notP1type_Msigma_nil ?FmaxM. have defM: H ><| U = M. by have [_] := kappa_compl_context maxM complU; rewrite defH K1 sdprodg1. @@ -1106,7 +1106,7 @@ have [K1 | ntK] := eqsVneq K 1. by exists p; rewrite // -p_rank_gt0 -(rank_Sylow sylP) rank_gt0. have PmaxM: M \in 'M_'P by rewrite inE -(trivg_kappa maxM hallK) ntK. have [Mstar _ [_ _ _ [cycW _ _ _ _]]] := Ptype_embedding PmaxM hallK. -case=> [[tiV _ _] _ _ defM {Mstar}]. +case=> [[tiV _ _] _ _ defM {Mstar}]. have [_ [_ cycK] [_ nUK _ _ _] _] := BGsummaryA maxM complU; rewrite -/H. case=> [[ntKs defCMK] [_ _ _ _ nilM'H] [sM''F defF /(_ ntK)sFM'] types34]. have hallK_M := pHall_Hall hallK. @@ -1280,7 +1280,7 @@ have tiA0A x a: x \in 'A0(M) :\: 'A(M) -> x ^ a \notin 'A(M). rewrite 3!inE; case: (x \in _) => //= /and3P[_ notM'x _]. apply: contra notM'x => /bigcupP[y _ /setD1P[_ /setIP[Mx _]]]. by rewrite -(p_eltJ _ _ a) (mem_p_elt (pgroup_pi _)). -have tiA0 x a: x \in 'A0(M) :\: 'A1(M) -> x ^ a \in 'A0(M) -> a \in M. +have tiA0 x a: x \in 'A0(M) :\: 'A1(M) -> x ^ a \in 'A0(M) -> a \in M. case/setDP=> A0x notA1x A0xa. have [Mx Mxa] := (subsetP sA0M x A0x, subsetP sA0M _ A0xa). have [[U K] /= complU] := kappa_witness maxM. @@ -1329,7 +1329,7 @@ have [FmaxM t2'M]: M \in 'M_'F /\ \tau2(M)^'.-group M. apply: (non_disjoint_signalizer_Frobenius ell1x MSx_gt1 SMxM). by apply: contra not_sNx'CMy; apply: pgroupS (subsetIl _ _). have defA0: 'A0(M) = Ms^#. - rewrite FTsupp0_type1; last by rewrite -FTtype_Fmax. + rewrite FTsupp0_type1; last by rewrite -FTtype_Fmax. rewrite /'A(M) /'A1(M) -FTtype_Fmax // FmaxM def_FTcore //= -/Ms. apply/setP => z; apply/bigcupP/idP=> [[t Ms1t] | Ms1z]; last first. have [ntz Ms_z] := setD1P Ms1z. diff --git a/mathcomp/odd_order/BGsection2.v b/mathcomp/odd_order/BGsection2.v index 5d7a899..85b95b2 100644 --- a/mathcomp/odd_order/BGsection2.v +++ b/mathcomp/odd_order/BGsection2.v @@ -134,7 +134,7 @@ without loss closF: F rG absG / group_closure_field F gT. move=> IH; apply: (@group_closure_field_exists gT F) => [[F' f closF']]. by apply: IH (map_repr f rG) _ closF'; rewrite map_mx_abs_irr. elim: {G}_.+1 {-2}G (ltnSn #|G|) => // m IHm G leGm in n rG absG solG *. -have [G1 | ntG] := eqsVneq G 1%g. +have [G1 | ntG] := eqsVneq G 1%g. by rewrite abelian_abs_irr ?G1 ?abelian1 // in absG; rewrite (eqP absG) dvd1n. have [H nsHG p_pr] := sol_prime_factor_exists solG ntG. set p := #|G : H| in p_pr. @@ -159,7 +159,7 @@ have card_sH: #|sH| = #|G : 'C_G[W | 'Cl]|. have /imsetP[W' _ defW'] := Clifford_atrans irrG sH. have WW': W' \in orbit 'Cl G W by rewrite orbit_in_sym // -defW' inE. by rewrite defW' andbT; apply/subsetP=> W'' /orbit_in_trans->. - rewrite orbit_stabilizer // card_in_imset //. + rewrite orbit_stabilizer // card_in_imset //. exact: can_in_inj (act_reprK _). have sHcW: H \subset 'C_G[W | 'Cl]. apply: subset_trans (subset_trans (joing_subl _ _) (Clifford_astab sH)) _. @@ -882,7 +882,7 @@ have{IHm} abelQ: abelian Q. move/forallP/(_ P); apply: contraL; rewrite subsetI subxx => -> /=. apply: contra ntQ'; rewrite /Q => /eqP->. by rewrite (setIidPr _) ?sub1G // commG1. - case/eqP: ntQ'; have{p'Q'}: P :&: Q^`(1)%g = 1%g. + case/eqP: ntQ'; have{p'Q'}: P :&: Q^`(1)%g = 1%g. rewrite coprime_TIg ?(pnat_coprime (pHall_pgroup sylP)) //= -/Q. by rewrite (pi_p'nat p'Q') // !inE p_pr. by rewrite (setIidPr _) // comm_subG ?subsetIr. @@ -925,7 +925,7 @@ have ap1: a ^+ p = 1. have ab1: a * b = 1. have: Q \subset <<[set y in G | \det (rG y) == 1]>>. rewrite subIset // genS //; apply/subsetP=> yz; case/imset2P=> y z Gy Gz ->. - rewrite inE !repr_mxM ?groupM ?groupV //= !detM (mulrCA _ (\det (rG y))). + rewrite inE !repr_mxM ?groupM ?groupV //= !detM (mulrCA _ (\det (rG y))). rewrite -!det_mulmx -!repr_mxM ?groupM ?groupV //. by rewrite mulKg mulVg repr_mx1 det1. rewrite gen_set_id; last first. @@ -1034,7 +1034,7 @@ pose B := col_mx u v; have uB: B \in unitmx. by rewrite mulmx1 -addsmxE addsmxS ?defU ?defUc. have Umod: mxmodule rP U by apply: rfix_mx_module. pose W := rfix_mx (factmod_repr Umod) P. -have ntW: W != 0. +have ntW: W != 0. apply: (rfix_pgroup_char charFp) => //. rewrite eqmxMfull ?row_full_unit ?unitmx_inv ?row_ebase_unit //. by rewrite rank_copid_mx -(eqP Uscal). diff --git a/mathcomp/odd_order/BGsection3.v b/mathcomp/odd_order/BGsection3.v index 007aaf4..5e9f5db 100644 --- a/mathcomp/odd_order/BGsection3.v +++ b/mathcomp/odd_order/BGsection3.v @@ -123,7 +123,7 @@ have fixsum (H : {group gT}): H \subset G -> (gsum H <= rfix_mx rG H)%MS. move/subsetP=> sHG; apply/rfix_mxP=> x Hx; have Gx := sHG x Hx. rewrite -gring_opG // -gring_opM ?envelop_mx_id //; congr (gring_op _ _). rewrite {2}/gset_mx (reindex_acts 'R _ Hx) ?astabsR //= mulmx_suml. - by apply:eq_bigr=> y; move/sHG=> Gy; rewrite repr_mxM. + by apply: eq_bigr=> y; move/sHG=> Gy; rewrite repr_mxM. have: gsum G + rG 1 *+ #|K| = gsum K + \sum_(x in K) gsum (R :^ x). rewrite -gring_opG // -sumr_const -!linear_sum -!linearD; congr gring_op. rewrite {1}/gset_mx (set_partition_big _ (Frobenius_partition frobG)) /=. @@ -350,7 +350,7 @@ have [nsKG sRG defKR nKR tiKR] := sdprod_context defG. have [sKG nKG] := andP nsKG; have solK := solvableS sKG solG. have cycR := prime_cyclic p_pr. case: (eqsVneq K 1) => [-> | ntK]; first by rewrite derg1 commG1 sub1G. -have defR x: x \in R^# -> <[x]> = R. +have defR x: x \in R^# -> <[x]> = R. case/setD1P; rewrite -cycle_subG -cycle_eq1 => ntX sXR. apply/eqP; rewrite eqEsubset sXR; apply: contraR ntX => /(prime_TIg p_pr). by rewrite /= (setIidPr sXR) => ->. @@ -856,7 +856,7 @@ have{IHsub nVH} IHsub: forall X : {group gT}, rewrite sub_Hall_pcore //; last by rewrite -defP commSg ?joing_subr. rewrite /pHall pcore_sub pcore_pgroup /= -(pseries_pop2 _ Op'HR0). rewrite -card_quotient ?normal_norm ?pseries_normal // -/(pgroup _ _). - by rewrite -{1}((_ :=P: _) p1_HR0) (quotient_pseries [::_;_]) pcore_pgroup. + by rewrite -{1}((_ :=P: _) p1_HR0) (quotient_pseries [::_; _]) pcore_pgroup. apply/trivgP; have <-: K :&: 'O_p([~: H0, R0]) = 1. by rewrite setIC coprime_TIg // (pnat_coprime (pcore_pgroup p _)). by rewrite commg_subI // subsetI ?sPOpHR0 ?sXK //= gFnorm_trans // normsRl. @@ -953,7 +953,7 @@ have iK'K: 'C_(P <*> R / K')(K / K') = 1 -> #|K / K'| > q ^ 2. by rewrite /pgroup (pi_pnat rR) // (pi_pnat pP) // !inE eq_sym. case cKK: (abelian K); last first. have [|[dPhiK dK'] dCKP] := abelian_charsimple_special qK coKP defKP. - apply/bigcupsP=> L /andP[charL]; have sLK := char_sub charL. + apply/bigcupsP=> L /andP[charL]; have sLK := char_sub charL. by case/IHsub: sLK cKK => // [|-> -> //]; apply: char_norm_trans charL _. have eK: exponent K %| q. have oddK: odd #|K| := oddSg sKG oddG. @@ -1395,7 +1395,7 @@ have chF: 'F(K) \char K := Fitting_char K; have nFR := char_norm_trans chF nKR. have nsFK := char_normal chF; have [sFK nFK] := andP nsFK. pose KqF := K / 'F(K); have solK := solvableS sKG solG. without loss [p p_pr pKqF]: / exists2 p, prime p & p.-group KqF. - move=> IHp; apply: wlog_neg => IH_KR; rewrite -quotient_cents2 //= -/KqF. + move=> IHp; apply: wlog_neg => IH_KR; rewrite -quotient_cents2 //= -/KqF. set Rq := R / 'F(K); have nKRq: Rq \subset 'N(KqF) by apply: quotient_norms. rewrite centsC. apply: subset_trans (coprime_cent_Fitting nKRq _ _); last first. @@ -1487,7 +1487,7 @@ have defKv: (P / V) * 'C_(G / V)(W) = (K / V). rewrite (subset_trans (quotientS _ sK_PF)) // quotientMl // mulgS //. rewrite subsetI -quotient_astabQ !quotientS //. by rewrite (subset_trans (Fitting_stab_chief solG nsKG)) ?(bigcap_inf (U, V)). -have nW_ := subset_trans (quotientS _ _) nWG; have nWK := nW_ _ sKG. +have nW_ := subset_trans (quotientS _ _) nWG; have nWK := nW_ _ sKG. rewrite -quotient_cents2 ?norms_cent ?(nW_ _ sRG) //. have [eq_qp | p'q] := eqVneq q p. apply: subset_trans (sub1G _); rewrite -trivg_quotient quotientS // centsC. diff --git a/mathcomp/odd_order/BGsection4.v b/mathcomp/odd_order/BGsection4.v index 217f151..c35c9ab 100644 --- a/mathcomp/odd_order/BGsection4.v +++ b/mathcomp/odd_order/BGsection4.v @@ -47,7 +47,7 @@ Proposition exponent_odd_nil23 gT (R : {group gT}) p : Proof. move=> pR oddR classR. pose f n := 'C(n, 3); pose g n := 'C(n, 3).*2 + 'C(n, 2). -have fS n: f n.+1 = 'C(n, 2) + f n by rewrite /f binS addnC. +have fS n: f n.+1 = 'C(n, 2) + f n by rewrite /f binS addnC. have gS n: g n.+1 = 'C(n, 2).*2 + 'C(n, 1) + g n. by rewrite /g !binS doubleD -!addnA; do 3!nat_congr. have [-> | ntR] := eqsVneq R 1. @@ -64,7 +64,7 @@ have exp_dv_p x m (S : {group gT}): - move=> expSp p_dv_m Sx; apply/eqP; rewrite -order_dvdn. by apply: dvdn_trans (dvdn_trans expSp p_dv_m); apply: dvdn_exponent. have p3_L21: p <= 3 -> {in R & &, forall u v w, [~ u, v, w] = 1}. - move=> lep3 u v w Ru Rv Rw; rewrite (ltnNge 3) lep3 nil_class2 in classR. + move=> lep3 u v w Ru Rv Rw; rewrite (ltnNge 3) lep3 nil_class2 in classR. by apply/eqP/commgP; red; rewrite (centerC Rw) // (subsetP classR) ?mem_commg. have{fS gS} expMR_fg: {in R &, forall u v n (r := [~ v, u]), (u * v) ^+ n = u ^+ n * v ^+ n * r ^+ 'C(n, 2) @@ -79,7 +79,7 @@ have{fS gS} expMR_fg: {in R &, forall u v n (r := [~ v, u]), rewrite -commuteM; try by apply: commuteX; red; rewrite cRr ?groupM. rewrite -mulgA; do 2!rewrite (mulgA _ u) (commgC _ u) -2!mulgA. congr (_ * (_ * _)); rewrite (mulgA _ v). - have ->: [~ v ^+ n, u] = r ^+ n * [~ r, v] ^+ 'C(n, 2). + have ->: [~ v ^+ n, u] = r ^+ n * [~ r, v] ^+ 'C(n, 2). elim: n => [|n IHn]; first by rewrite comm1g mulg1. rewrite !expgS commMgR -/r {}IHn commgX; last exact: cRr. rewrite binS bin1 addnC expgD -2!mulgA; congr (_ * _); rewrite 2!mulgA. @@ -168,7 +168,7 @@ have [[x y] genR modR] := generators_modular_group p_pr e_gt1 isoR. have [_ _ _ _] := modular_group_structure p_pr e_gt1 genR isoR modR. rewrite xpair_eqE p2; case/(_ 1%N) => // _ oR1. by rewrite 2!inE Ohm_sub oR1 pfactorK ?abelem_Ohm1 ?(card_p2group_abelian p_pr). -Qed. +Qed. Section OddNonCyclic. @@ -197,7 +197,7 @@ Qed. (* This is B & G, Lemma 4.5(c). *) Lemma Ohm1_odd_ucn2 (Z := 'Ohm_1('Z_2(R))) : ~~ cyclic Z /\ exponent Z %| p. -Proof. +Proof. have [S nsSR Ep2S] := ex_odd_normal_p2Elem; have p_pr := pnElem_prime Ep2S. have [sSR abelS dimS] := pnElemP Ep2S; have [pS cSS expSp]:= and3P abelS. pose SR := [~: S, R]; pose SRR := [~: SR, R]. @@ -209,7 +209,7 @@ have sSR_R := subset_trans sSR_S sSR. have{ntS} prSR: SR \proper S. by rewrite (nil_comm_properl nilR) // subsetI subxx -commg_subl. have SRR1: SRR = 1. - have [SR1 | ntSR] := eqVneq SR 1; first by rewrite /SRR SR1 comm1G. + have [SR1 | ntSR] := eqVneq SR 1; first by rewrite /SRR SR1 comm1G. have prSRR: SRR \proper SR. rewrite /proper sSRR_SR; apply: contra ntSR => sSR_SRR. by rewrite (forall_inP nilR) // subsetI sSR_R. @@ -303,7 +303,7 @@ have{gtR2} [A] := p_rank_geP gtR2; pose H := 'C_A(Z); pose K := H <*> Z. case/pnElemP=> sAR abelA dimA3; have [pA cAA _] := and3P abelA. have{nsZR} nZA := subset_trans sAR (normal_norm nsZR). have sHA: H \subset A := subsetIl A _; have abelH := abelemS sHA abelA. -have geH2: logn p #|H| >= 2. +have geH2: logn p #|H| >= 2. rewrite -ltnS -dimA3 -(Lagrange sHA) lognM // -addn1 leq_add2l /= -/H. by rewrite logn_quotient_cent_abelem ?dimZ2. have{abelH} abelK : p.-abelem K. @@ -330,7 +330,7 @@ have sAR := normal_sub nAR; have pA := pgroupS sAR pR. have abelA : p.-abelem A. by rewrite /abelem pA cAA /= (dvdn_trans (exponentS sAR) expR). have cardA : logn p #|A| <= 2. - by rewrite -rank_abelem // (leq_trans (rankS sAR) rankR). + by rewrite -rank_abelem // (leq_trans (rankS sAR) rankR). have cardRA : logn p #|R : A| <= 1. by rewrite -cRAA logn_quotient_cent_abelem // (normal_norm nAR). rewrite -(Lagrange sAR) lognM ?cardG_gt0 //. @@ -384,7 +384,7 @@ have dimS1b: logn p #|R / 'Ohm_1(S)| <= 1. by rewrite dvdn_leq_log ?prime_gt0 // order_dvdn yp1. rewrite (leq_trans (nil_class_pgroup pR)) // geq_max /= -subn1 leq_subLR. by rewrite -(Lagrange sS1R) lognM // -card_quotient // addnC leq_add. -Qed. +Qed. (* This is B & G, Lemma 4.9. *) Lemma quotient_p2_Ohm1 gT p (R : {group gT}) : @@ -495,7 +495,7 @@ have [cRR | not_cRR] := boolP (abelian R). by rewrite big_seq1 => <-; rewrite cyclic_metacyclic ?cycle_cyclic. rewrite big_cons big_seq1; case/dprodP=> _ <- cAB _. apply/existsP; exists <[a]>%G; rewrite cycle_cyclic /=. - rewrite /normal mulG_subl mulG_subG normG cents_norm //= quotientMidl. + rewrite /normal mulG_subl mulG_subG normG cents_norm //= quotientMidl. by rewrite quotient_cycle ?cycle_cyclic // -cycle_subG cents_norm. pose R' := R^`(1); pose e := 'Mho^1(R') != 1. have nsR'R: R' <| R := der_normal 1 R; have [sR'R nR'R] := andP nsR'R. @@ -757,7 +757,7 @@ case recR: [exists (S : {group gT} | S \proper R), a \in 'N(S) :\: 'C(S)]. by apply: IHn nSa oa _; rewrite ?(pgroupS sSR) ?(leq_trans ltSR). do [rewrite inE -!cycle_subG orderE; set A := <[a]>] in nRa oa. have{nRa oa} [[not_cRA nRA] oA] := (andP nRa, oa). -have coRA : coprime #|R| #|A| by rewrite oA (pnat_coprime pR) ?pnatE. +have coRA : coprime #|R| #|A| by rewrite oA (pnat_coprime pR) ?pnatE. have{recR} IH: forall S, gval S \proper R -> A \subset 'N(S) -> A \subset 'C(S). move=> S ltSR; rewrite !cycle_subG => nSa; apply: contraFT recR => not_cSa. by apply/exists_inP; exists S; rewrite // inE not_cSa nSa. @@ -929,9 +929,9 @@ have{ziTX defB1} cycX: cyclic X; last have [x defX]:= cyclicP cycX. have{Xb defXb defBb nsCX} mulSX: S * X = R. have nCT: T \subset 'N(C) := subset_trans sTR nCR. rewrite -defR -(normC (subset_trans sSR nBR)) -[B](quotientGK nsCB) -defBb. - rewrite cosetpreM quotientK // defXb quotientGK // -(normC nCT). + rewrite cosetpreM quotientK // defXb quotientGK // -(normC nCT). by rewrite -mulgA (mulSGid sCX) mulgA (mulGSid sTS). -have{mulSX} not_sXS_S': ~~ ([~: X, S] \subset S'). +have{mulSX} not_sXS_S': ~~ ([~: X, S] \subset S'). apply: contra not_sTS' => sXS_S'; rewrite /T -mulSX. by rewrite commGC commMG ?(subset_trans sXR) // mul_subG. have [oSb oTb] : #|S / T| = p /\ #|T / S'| = p. @@ -993,7 +993,7 @@ have i_neq0: i != 0 %[mod p]. rewrite -(orderJ _ a) conjXg xa order_eq1 -expgM -order_dvdn mod0n. apply: contra; case/dvdnP=> m ->; rewrite -mulnA -expnS dvdn_mull //. by rewrite {1}[#[x]](card_pgroup pX) dvdn_exp2l ?leqSpred. -have Txy: [~ x, y] \in T by rewrite [T]commGC mem_commg // -cycle_subG -defX. +have Txy: [~ x, y] \in T by rewrite [T]commGC mem_commg // -cycle_subG -defX. have [Rx Ry]: x \in R /\ y \in R by rewrite -cycle_subG -defX (subsetP sSR). have [nS'x nS'y] := (subsetP nS'R x Rx, subsetP nS'R y Ry). have{not_sXS_S'} not_S'xy: [~ x, y] \notin S'. @@ -1077,7 +1077,7 @@ have s_p'C_B X: gval X \subset C -> p^'.-group X -> X \subset B. by rewrite qact_domE ?acts_char. rewrite gacentE // subsetIidl -/V; apply/subsetP=> v Vv; apply/afixP=> a Xa. have [cVa dom_a] := (subsetP sXC a Xa, subsetP domXb a Xa). - have [x Nx Hx def_v] := morphimP Vv; rewrite {1}def_v qactE //=. + have [x Nx Hx def_v] := morphimP Vv; rewrite {1}def_v qactE //=. by rewrite -qactE ?(astab_dom cVa) ?(astab_act cVa) -?def_v. have{B pB s_p'C_B} pC : p.-group C. apply/pgroupP=> q q_pr /Cauchy[] // a Ca oa; apply: wlog_neg => p'q. @@ -1107,7 +1107,7 @@ rewrite !inE; case/pred2P=> dimV. pose Vb := sdpair1 toAV @* V; pose Ab := sdpair2 toAV @* A. have [injV injA] := (injm_sdpair1 toAV, injm_sdpair2 toAV). have abelVb: p.-abelem Vb := morphim_abelem _ abelV. -have ntVb: Vb != 1 by rewrite morphim_injm_eq1. +have ntVb: Vb != 1 by rewrite morphim_injm_eq1. have nVbA: Ab \subset 'N(Vb) := im_sdpair_norm toAV. pose rV := morphim_repr (abelem_repr abelVb ntVb nVbA) (subxx A). have{defC} <-: rker rV = C; last move: rV. @@ -1128,8 +1128,8 @@ without loss Gp'1: gT G solG oddG rG q_dv_G / 'O_p^'(G) = 1. rewrite trivg_pcore_quotient -(card_isog (quotient1_isog _)). by rewrite p_rank_p'quotient ?pcore_pgroup ?gFnorm //; apply. set R := 'O_p(G); have pR: p.-group R := pcore_pgroup p G. -have [sRG nRG] := andP (pcore_normal p G : R <| G). -have oddR: odd #|R| := oddSg sRG oddG. +have [sRG nRG] := andP (pcore_normal p G : R <| G). +have oddR: odd #|R| := oddSg sRG oddG. have rR: 'r(R) <= 2 by rewrite (rank_pgroup pR) (leq_trans _ rG) ?p_rankS. rewrite leq_eqVlt -implyNb; apply/implyP=> p'q. have [|//] := pi_Aut_rank2_pgroup pR oddR rR _ p'q; rewrite eq_sym in p'q. @@ -1193,7 +1193,7 @@ Qed. (* This is B & G, Theorem 4.18(d) *) Theorem rank2_sub_p'core_der1 gT (G A : {group gT}) p : solvable G -> odd #|G| -> 'r_p(G) <= 2 -> p^'.-subgroup(G^`(1)) A -> - A \subset 'O_p^'(G^`(1)). + A \subset 'O_p^'(G^`(1)). Proof. move=> solG oddG rG /andP[sAG' p'A]; rewrite sub_Hall_pcore //. by have [-> _ _] := rank2_der1_complement solG oddG rG. @@ -1264,7 +1264,7 @@ have pGb: p.-group((G / 'C_G(R))^`(1)). by rewrite defA -pgroupE (der1_Aut_rank2_pgroup pR) ?(oddSg sRG). set C := 'C_G(U / V | 'Q). have nUfG: [acts G, on U / V | 'Q] by rewrite actsQ. -have nCG: G \subset 'N(C) by rewrite -(setIidPl nUfG) normsGI ?astab_norm. +have nCG: G \subset 'N(C) by rewrite -(setIidPl nUfG) normsGI ?astab_norm. have{pGb sUfR} pGa': p.-group (G / C)^`(1). have nCRG : G \subset 'N('C_G(R)) by rewrite normsI ?normG ?norms_cent. have sCR_C: 'C_G(R) \subset C. diff --git a/mathcomp/odd_order/BGsection5.v b/mathcomp/odd_order/BGsection5.v index bf84a99..9769c86 100644 --- a/mathcomp/odd_order/BGsection5.v +++ b/mathcomp/odd_order/BGsection5.v @@ -69,7 +69,7 @@ Proof. move=> injf sHG; rewrite /narrow injm_p_rank //; congr (_ ==> _). apply/set0Pn/set0Pn=> [] [E /setIP[Ep2E maxE]]. exists (invm injf @* E)%G; rewrite -[H](group_inj (morphim_invm injf _)) //. - have sEfG: E \subset f @* G. + have sEfG: E \subset f @* G. by rewrite (subset_trans _ (morphimS _ sHG)) //; case/pnElemP: Ep2E. by rewrite inE injm_pnElem ?injm_pmaxElem ?injm_invm ?morphimS // Ep2E. have sEG: E \subset G by rewrite (subset_trans _ sHG) //; case/pnElemP: Ep2E. @@ -166,7 +166,7 @@ Proof. by rewrite Ohm1_eq1 (center_nil_eq1 (pgroup_nil pR)). Qed. Let sZR : Z \subset R. Proof. by rewrite !gFsub_trans. Qed. -Let abelZ : p.-abelem (Z). +Let abelZ : p.-abelem (Z). Proof. by rewrite (Ohm1_abelem (pgroupS _ pR)) ?center_sub ?center_abelian. Qed. Let pZ : p.-group Z. Proof. exact: abelem_pgroup abelZ. Qed. @@ -272,12 +272,12 @@ have sZT: Z \subset T. have{SZ sSSZ maxSZ} not_sST: ~~ (S \subset T). have: ~~ (SZ \subset T) by case/Ohm1_ucn_p2maxElem: maxSZ. by rewrite join_subG sZT andbT. -have tiST: S :&: T :=: 1 by rewrite prime_TIg ?oS. +have tiST: S :&: T :=: 1 by rewrite prime_TIg ?oS. have defST: S * T = R. apply/eqP; rewrite eqEcard TI_cardMg ?mul_subG ?subsetIl //=. - by rewrite mulnC oS -maxT Lagrange ?subsetIl. + by rewrite mulnC oS -maxT Lagrange ?subsetIl. have cRRb: abelian (R / T) by rewrite -defST quotientMidr quotient_abelian. -have sR'T: R^`(1) \subset T by rewrite der1_min ?char_norm. +have sR'T: R^`(1) \subset T by rewrite der1_min ?char_norm. have TI_SR': S :&: R^`(1) :=: 1. by rewrite prime_TIg ?oS // (contra _ not_sST) // => /subset_trans->. have defCRS : S \x 'C_T(S) = 'C_R(S). @@ -385,12 +385,12 @@ have tiHS: H :&: S = 1. have nsUR: U <| R. rewrite /normal sUR -commg_subl (subset_trans (commSg _ sUH)) //= -/U. by rewrite (subset_trans sHRZ) // joing_subr. - have{rU}:= leq_trans rU rCRS; rewrite leq_eqVlt => /predU1P[] rU. + have{rU}:= leq_trans rU rCRS; rewrite leq_eqVlt => /predU1P[] rU. have Ep2U: [group of U] \in 'E_p^2(R). by rewrite !inE /= sUR abelU -(p_rank_abelem abelU) rU. have [F scn3F sUF] := normal_p2Elem_SCN3 rR Ep2U nsUR. - have [scnF rF] := setIdP scn3F; have [_ scF] := SCN_P scnF. - rewrite (leq_trans rF) // -scF -rank_pgroup ?(pgroupS (subsetIl _ _)) //. + have [scnF rF] := setIdP scn3F; have [_ scF] := SCN_P scnF. + rewrite (leq_trans rF) // -scF -rank_pgroup ?(pgroupS (subsetIl _ _)) //. by rewrite rankS ?setIS ?centS // (subset_trans _ sUF) ?joing_subl. have defU: S :=: U. apply/eqP; rewrite eqEcard oS joing_subl (card_pgroup (pgroupS sUR pR)). @@ -424,7 +424,7 @@ suffices pB (X : {group {perm gT}}): X \subset B -> p^'.-group X -> X :=: 1. rewrite -partn_eq1 ?cardG_gt0 // -(card_Hall sylX). by rewrite (pB X) ?cards1 ?(pi_pgroup qX) ?(subset_trans sXA') ?joing_subl. rewrite cAbAb -(nilpotent_pcoreC p (abelian_nil cAbAb)) trivg_pcore_quotient. - rewrite dprod1g pcore_pgroup; split=> //_ a Aa p'a. + rewrite dprod1g pcore_pgroup; split=> //_ a Aa p'a. rewrite order_dvdn -cycle_eq1 [<[_]>]pB ?(pgroupS (cycleX _ _) p'a) //. by rewrite genS // sub1set inE orbC (mem_imset (expgn^~ _)). move=> sXB p'X; have AutX := subset_trans sXB AutB. @@ -478,7 +478,7 @@ apply: dvdn_trans (order_dvdG (actperm_Aut _ Dx)) _. by rewrite card_Aut_cyclic // oLb (@totient_pfactor p 1) ?muln1. Qed. -End OneGroup. +End OneGroup. (* This is B & G, Theorem 5.6, parts (a) and (c). We do not prove parts (b), *) (* (d) and (e), as they are not used in the proof of the Odd Order Theorem. *) diff --git a/mathcomp/odd_order/BGsection6.v b/mathcomp/odd_order/BGsection6.v index e344b98..9e06b1a 100644 --- a/mathcomp/odd_order/BGsection6.v +++ b/mathcomp/odd_order/BGsection6.v @@ -31,7 +31,7 @@ Implicit Type p : nat. Section OneType. -Variable gT : finGroupType. +Variable gT : finGroupType. Implicit Types G H K S U : {group gT}. (* This is B & G, Theorem A.4(b) and 6.1, or Gorenstein 6.5.2, the main Hall- *) @@ -77,7 +77,7 @@ case/sdprodP=> _ defG nKH tiKH coKH solK sKG'. set K' := K^`(1); have [sK'K nK'K] := andP (der_normal 1 K : K' <| K). have nK'H: H \subset 'N(K') := gFnorm_trans _ nKH. set R := [~: K, H]; have sRK: R \subset K by rewrite commg_subl. -have [nRK nRH] := joing_subP (commg_norm K H : K <*> H \subset 'N(R)). +have [nRK nRH] := joing_subP (commg_norm K H : K <*> H \subset 'N(R)). have sKbK'H': K / R \subset (K / R)^`(1) * (H / R)^`(1). have defGb: (K / R) \* (H / R) = G / R. by rewrite -defG quotientMl ?cprodE // centsC quotient_cents2r. @@ -90,7 +90,7 @@ have{sKbK'H' tiKbHb'} derKb: (K / R)^`(1) = K / R. have{derKb} Kb1: K / R = 1. rewrite (contraNeq (sol_der1_proper _ (subxx (K / R)))) ?quotient_sol //. by rewrite derKb properxx. -have{Kb1 sRK} defKH: [~: K, H] = K. +have{Kb1 sRK} defKH: [~: K, H] = K. by apply/eqP; rewrite eqEsubset sRK -quotient_sub1 ?Kb1 //=. split=> //; rewrite -quotient_sub1 ?subIset ?nK'K //= -/K'. have cKaKa: abelian (K / K') := der_abelian 0 K. @@ -255,7 +255,7 @@ Qed. (* This is B & G, Lemma 6.6(d). *) Lemma plength1_Sylow_Jsub (Q : {group gT}) : Q \subset G -> p.-group Q -> - exists2 x, x \in 'C_G(Q :&: S) & Q :^ x \subset S. + exists2 x, x \in 'C_G(Q :&: S) & Q :^ x \subset S. Proof. move=> sQG pQ; have sQ_Gp'p: Q \subset 'O_{p^',p}(G). rewrite -sub_quotient_pre /= pcore_mod1 ?(subset_trans sQG) //. @@ -278,7 +278,7 @@ End OneType. Theorem plength1_norm_pmaxElem gT p (G E L : {group gT}) : E \in 'E*_p(G) -> odd p -> solvable G -> p.-length_1 G -> L \subset G -> E \subset 'N(L) -> p^'.-group L -> - L \subset 'O_p^'(G). + L \subset 'O_p^'(G). Proof. move=> maxE p_odd solG pl1G sLG nEL p'L. case p_pr: (prime p); last first. diff --git a/mathcomp/odd_order/BGsection7.v b/mathcomp/odd_order/BGsection7.v index 71e800e..5f803b0 100644 --- a/mathcomp/odd_order/BGsection7.v +++ b/mathcomp/odd_order/BGsection7.v @@ -770,9 +770,9 @@ End NormedConstrained. Proposition plength_1_normed_constrained p A : A :!=: 1 -> A \in 'E*_p(G) -> (forall M, M \proper G -> p.-length_1 M) -> normed_constrained A. -Proof. +Proof. move=> ntA EpA pl1subG. -case/pmaxElemP: (EpA); case/pElemP=> sAG; case/and3P=> pA cAA _ _. +case/pmaxElemP: (EpA); case/pElemP=> sAG; case/and3P=> pA cAA _ _. have prA: A \proper G := sub_proper_trans cAA (mFT_cent_proper ntA). split=> // X Y sAX prX; case/setIdP; case/andP=> sYX p'Y nYA. have pl1X := pl1subG _ prX; have solX := mFT_sol prX. diff --git a/mathcomp/odd_order/BGsection8.v b/mathcomp/odd_order/BGsection8.v index db378f3..513d6d1 100644 --- a/mathcomp/odd_order/BGsection8.v +++ b/mathcomp/odd_order/BGsection8.v @@ -68,7 +68,7 @@ have piCA: pi.-group('C(A)). have Mx := subsetP sCAM x cAx; pose C := 'C_F(<[x]>). have sAC: A \subset C by rewrite subsetI sAF centsC cycle_subG. have sCFC_C: 'C_F(C) \subset C. - by rewrite (subset_trans _ sAC) ?setIS // centS ?(subset_trans _ sAC). + by rewrite (subset_trans _ sAC) ?setIS // centS ?(subset_trans _ sAC). have cFx: x \in 'C_M(F). rewrite inE Mx -cycle_subG coprime_nil_faithful_cent_stab //=. by rewrite cycle_subG (subsetP (gFnorm _ _)). @@ -339,7 +339,7 @@ have prH: H \proper G by rewrite inE in maxH; apply: maxgroupp maxH. have sAHM: A \subset H :&: M by rewrite subsetI sAH. have [R sylR_HM sAR]:= Sylow_superset sAHM (pgroupS sAP pP). have [/subsetIP[sRH sRM] pR _] := and3P sylR_HM. -have{sylR_HM} sylR_H: p.-Sylow(H) R. +have{sylR_HM} sylR_H: p.-Sylow(H) R. have [Q sylQ] := Sylow_superset sRM pR; have [sQM pQ _] := and3P sylQ. case/eqVproper=> [defR | /(nilpotent_proper_norm (pgroup_nil pQ)) sRN]. apply: (pHall_subl sRH (subsetT _)); rewrite pHallE subsetT /=. diff --git a/mathcomp/odd_order/BGsection9.v b/mathcomp/odd_order/BGsection9.v index f649e84..fe2b86a 100644 --- a/mathcomp/odd_order/BGsection9.v +++ b/mathcomp/odd_order/BGsection9.v @@ -372,14 +372,14 @@ have uNP0_mCA M: M \in 'M('C(A)) -> 'M('N(P0)) = [set M]. have nVU := subset_trans sUDL (subset_trans sDL nV_LM). rewrite IHs ?(subset_trans sVU) // /stable_factor /normal sVU nVU !andbT. have nVP0 := subset_trans (subset_trans sP0_LM' (der_sub _ _)) nV_LM. - rewrite commGC -sub_astabQR // (subset_trans sP0_LM') //. + rewrite commGC -sub_astabQR // (subset_trans sP0_LM') //. have /is_abelemP[q _ /andP[qUV _]]: is_abelem (U / V). exact: sol_chief_abelem solLM chUV. apply: rank2_der1_cent_chief qUV sUDL; rewrite ?mFT_odd //. exact: leq_trans (p_rank_le_rank _ _) DLle2. rewrite centsC (subset_trans cDL_P0) ?centS ?setIS //. by rewrite (subset_trans _ sCxL) // -cent_set1 centS ?sub1set. - case: (ltnP 2 'r(F)) => [| Fle2]. + case: (ltnP 2 'r(F)) => [| Fle2]. have [q q_pr -> /= Fq3] := rank_witness [group of F]. have Mq3: 'r('O_q(M)) >= 3. rewrite (rank_pgroup (pcore_pgroup _ _)) /= -p_core_Fitting. diff --git a/mathcomp/odd_order/PFsection1.v b/mathcomp/odd_order/PFsection1.v index 1d784ed..8e0b539 100644 --- a/mathcomp/odd_order/PFsection1.v +++ b/mathcomp/odd_order/PFsection1.v @@ -196,7 +196,7 @@ Lemma vchar_isometry_base m L (Chi : m.-tuple 'CF(H)) uniq mu & exists epsilon : bool, forall i : 'I_m, tau (Chi`_i - Chi`_0) = (-1) ^+ epsilon *: ('chi_(mu`_i) - 'chi_(mu`_0)). -Proof. +Proof. case: m Chi => [|[|m]] // Chi _ irrChi Chifree Chi1 ChiCF [iso_tau Ztau]. rewrite -(tnth_nth 0 _ 0); set chi := tnth Chi. have chiE i: chi i = Chi`_i by rewrite -tnth_nth. @@ -272,7 +272,7 @@ rewrite (partition_big (conjg_Iirr t) xpredT) //=; apply: eq_bigr => i _. have [[y Gy chi_i] | not_i_t] := cfclassP _ _ _; last first. apply: big1 => z; rewrite groupV => /andP[Gz /eqP def_i]. by case: not_i_t; exists z; rewrite // -def_i conjg_IirrE. -rewrite -(card_rcoset _ y) mulr_natl -sumr_const; apply: eq_big => z. +rewrite -(card_rcoset _ y) mulr_natl -sumr_const; apply: eq_big => z. rewrite -(inj_eq irr_inj) conjg_IirrE chi_i mem_rcoset inE groupMr ?groupV //. apply: andb_id2l => Gz; rewrite eq_sym (cfConjg_eqE _ nsHG) //. by rewrite mem_rcoset inE groupM ?groupV. @@ -315,7 +315,7 @@ Qed. (* Useful consequences of (1.5)(c) *) Lemma not_cfclass_Ind_ortho i j : H <| G -> ('chi_i \notin 'chi_j ^: G)%CF -> - '['Ind[G, H] 'chi_i, 'Ind[G, H] 'chi_j] = 0. + '['Ind[G, H] 'chi_i, 'Ind[G, H] 'chi_j] = 0. Proof. by move/(cfclass_Ind_cases i j); rewrite cfclass_sym; case: ifP. Qed. Lemma cfclass_Ind_irrP i j : @@ -363,7 +363,7 @@ Qed. (* This is Peterfalvi (1.5)(e). *) Lemma odd_induced_orthogonal t : H <| G -> odd #|G| -> t != 0 -> - '['Ind[G, H] 'chi_t, ('Ind[G] 'chi_t)^*] = 0. + '['Ind[G, H] 'chi_t, ('Ind[G] 'chi_t)^*] = 0. Proof. move=> nsHG oddG nz_t; have [sHG _] := andP nsHG. have:= cfclass_Ind_cases t (conjC_Iirr t) nsHG. @@ -582,7 +582,7 @@ have I1B: 'chi_i1 1%g ^+ 2 <= #|C : D|%:R. move/ler_trans; apply. rewrite ler_nat // -(index_quotient_eq CBsH) ?normal_norm //. rewrite -(@leq_pmul2l #|'Z('chi_i2)%CF|) ?cardG_gt0 ?cfcenter_sub //. - rewrite Lagrange ?quotientS ?cfcenter_sub //. + rewrite Lagrange ?quotientS ?cfcenter_sub //. rewrite -(@leq_pmul2l #|(D / B)%g|) ?cardG_gt0 //. rewrite mulnA mulnAC Lagrange ?quotientS //. rewrite mulnC leq_pmul2l ?cardG_gt0 // subset_leq_card //. diff --git a/mathcomp/odd_order/PFsection10.v b/mathcomp/odd_order/PFsection10.v index 11b3b20..03d8898 100644 --- a/mathcomp/odd_order/PFsection10.v +++ b/mathcomp/odd_order/PFsection10.v @@ -417,14 +417,14 @@ have al_ij_zeta_s: '[al_ij^\tau, zeta^*^\tau1] = a. have M'dz: zeta - zeta^*%CF \in 'Z[calS, M'^#] by apply: seqInd_sub_aut_zchar. rewrite Dtau1 // Dade_isometry ?alpha_on ?tauM' //. rewrite cfdotBr opprB cfdotBl cfdot_conjCr rmorphB linearZ /=. - rewrite -!prTIirr_aut !cfdotBl !cfdotZl !o_mu2_zeta o_zeta_s !mulr0. + rewrite -!prTIirr_aut !cfdotBl !cfdotZl !o_mu2_zeta o_zeta_s !mulr0. by rewrite opprB !(subr0, rmorph0) add0r irrWnorm ?mulr1. have Zal_ij: al_ij^\tau \in 'Z[irr G] by apply: Zalpha_tau. have Za: a \in Cint. by rewrite rpredD ?(Cint_Cnat Nn) ?Cint_cfdot_vchar ?Ztau1 ?(mem_zchar Szeta). have{al_ij_zeta_s} ub_da2: (d ^ 2)%:R * a ^+ 2 <= (2%:R + n ^+ 2) * w1%:R. have [k nz_k j'k]: exists2 k, k != 0 & k != j. - have:= w2gt2; rewrite -nirrW2 (cardD1 0) (cardD1 j) !inE nz_j !ltnS lt0n. + have:= w2gt2; rewrite -nirrW2 (cardD1 0) (cardD1 j) !inE nz_j !ltnS lt0n. by case/pred0Pn=> k /and3P[]; exists k. have muk_1: mu_ k 1%g = (d * w1)%:R. by rewrite (prTIred_1 pddM) mu1 // mulrC -natrM. @@ -437,7 +437,7 @@ have{al_ij_zeta_s} ub_da2: (d ^ 2)%:R * a ^+ 2 <= (2%:R + n ^+ 2) * w1%:R. by rewrite 2 1?eq_sym // mulr0 -mulrN opprB !subr0 add0r. have ZSmuk: mu_ k \in 'Z[calS] by rewrite mem_zchar ?calSmu. have <-: '[al_ij^\tau] * '[(mu_ k)^\tau1] = (2%:R + n ^+ 2) * w1%:R. - by rewrite Itau1 // cfdot_prTIred eqxx mul1n norm_alpha. + by rewrite Itau1 // cfdot_prTIred eqxx mul1n norm_alpha. by rewrite -Cint_normK ?cfCauchySchwarz // Cint_cfdot_vchar // Ztau1. suffices a0 : a = 0. by apply: (def_tau_alpha _ sSS0); rewrite // -sub0r -a0 addrK. @@ -1087,7 +1087,7 @@ have Dalpha i (al_ij := alpha_ i j) : by rewrite -mulrA !mulr_natl; case: (S1) => // in S1zeta lb_n2alij *. have{ub_a2} ub_8a2: 8%:R * a ^+ 2 <= 4%:R * a + 2%:R. rewrite mulrAC Dn -natrM in ub_a2; apply: ler_trans ub_a2. - rewrite -Cint_normK // ler_wpmul2r ?exprn_ge0 ?normr_ge0 // leC_nat szS1. + rewrite -Cint_normK // ler_wpmul2r ?exprn_ge0 ?normr_ge0 // leC_nat szS1. rewrite (subn_sqr p 1) def_p_w1 subnK ?muln_gt0 // mulnA mulnK // mulnC. by rewrite -subnDA -(mulnBr 2 _ 1%N) mulnA (@leq_pmul2l 4 2) ?ltn_subRL. have Z_4a1: 4%:R * a - 1%:R \in Cint by rewrite rpredB ?rpredM ?rpred_nat. diff --git a/mathcomp/odd_order/PFsection11.v b/mathcomp/odd_order/PFsection11.v index c37633f..3635618 100644 --- a/mathcomp/odd_order/PFsection11.v +++ b/mathcomp/odd_order/PFsection11.v @@ -151,7 +151,7 @@ by rewrite Frobenius_coprime_quotient ?gFnormal //; split=> // _ /prHUW1->. Qed. Let defHC : H \x C = HC. -Proof. +Proof. by have [defHC _ _ _] := typeP_context MtypeP; rewrite /= (dprodWY defHC). Qed. @@ -233,7 +233,7 @@ Lemma bounded_proper_coherent H1 : Proof. move=> nsH1_M psH1_M' cohH1; have [nsHHU _ _ _ _] := sdprod_context defHU. suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC. - rewrite indexgg sqrtC1 mulr1 -leC_nat natrD -ler_subl_addr -mulnA natrM. + rewrite indexgg sqrtC1 mulr1 -leC_nat natrD -ler_subl_addr -mulnA natrM. congr (_ <= _ * _%:R); apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 HC)). rewrite Lagrange ?normal_sub // mulnCA -(dprod_card defHC) -mulnA mulnC. by rewrite Lagrange ?subsetIl // (sdprod_card defHU) (sdprod_card defM). @@ -281,7 +281,7 @@ Local Notation defM'' := FTtype34_der2. (* This is Peterfalvi (11.6). *) Lemma FTtype34_facts (H' := H^`(1)%g): - [/\ p.-group H, U \subset 'C(H0), H0 :=: H' & C :=: U']. + [/\ p.-group H, U \subset 'C(H0), H0 :=: H' & C :=: U']. Proof. have nilH: nilpotent H := Fcore_nil M. have /sdprod_context[/andP[_ nHM] sUW1M _ _ _] := Ptype_Fcore_sdprod MtypeP. @@ -323,7 +323,7 @@ have{coH_UW1} defH0: H0 :=: H'. by have [_ _ _ <-] := dprodP defHUhat; rewrite setIC setIS ?der_sub. have coHUhat: coprime #|Hhat| #|Uhat|. by rewrite coprime_morph ?(coprimegS _ coH_UW1) ?joing_subl. - have defHhat: 'C_Hhat(Uhat) \x [~: Hhat, Uhat] = Hhat. + have defHhat: 'C_Hhat(Uhat) \x [~: Hhat, Uhat] = Hhat. by rewrite dprodC coprime_abelian_cent_dprod ?der_abelian ?quotient_norms. rewrite /HUhat -(sdprodWY defHU) quotientY //= -(dprodWY defHhat). have [_ _ cCRhat tiCRhat] := dprodP defHhat. @@ -342,7 +342,7 @@ have /subsetIP[sRH cUR]: R \subset 'C_H(U). rewrite (card_Hall (setI_normal_Hall _ hallR _)) ?subsetIl ?gFnormal //. rewrite partnM ?expn_gt0 ?cardG_gt0 //= part_p'nat ?mul1n ?pnatNK //. by rewrite pnat_exp ?pnat_id. -suffices: ~~ (R^`(1)%g \proper R) by apply: contraNeq (sol_der1_proper solH _). +suffices: ~~ (R^`(1)%g \proper R) by apply: contraNeq (sol_der1_proper solH _). have /setIidPr {2}<-: R \subset HU^`(1)%g. by rewrite [HU^`(1)%g]defM'' -(dprodWY defHC) sub_gen ?subsetU ?sRH. suffices defRHpU: R \x ('O_p(H) <*> U) = HU. @@ -521,7 +521,7 @@ have{oDx12} phi_w12 ubar: ubar \in Ubar -> (phi_ w1 ubar * phi_ w2 ubar = 1)%g. apply; apply/rcoset_kercosetP; rewrite ?groupX ?nH0H //. by rewrite morphX ?morphJ ?(nH0W1 w) // ?nH0H //= -Dubar -Dxbar xbarJ. rewrite -eq_expg_mod_order -{1}Dsym expgM expgVn ?(DXn, Dsym) ?Hx_ //. - rewrite /D -!morphR ?nQH ?Hx_ // -conjRg (conjg_fixP _) //. + rewrite /D -!morphR ?nQH ?Hx_ // -conjRg (conjg_fixP _) //. by apply/commgP/esym/(centsP cH0U); rewrite ?memH0 ?Hx_. pose wbar := bar (w1 * w2 ^-1)%g; pose W1bar := (W1 / H0)%g. have W1wbar: wbar \in W1bar by rewrite mem_quotient ?groupM ?groupV. @@ -646,7 +646,7 @@ Qed. Let Zbridge0 : {in S1, forall zeta, bridge0 zeta \in 'Z[irr M, HU^#]}. Proof. have mu0_1: mu_ 0 1%g = q%:R by rewrite prTIred_1 prTIirr0_1 mulr1. -move=> zeta S1zeta; rewrite /= zcharD1 !cfunE subr_eq0 mu0_1 S1_1 // eqxx. +move=> zeta S1zeta; rewrite /= zcharD1 !cfunE subr_eq0 mu0_1 S1_1 // eqxx. by rewrite rpredB ?(seqInd_vchar _ (Tmu 0)) ?(seqInd_vchar _ S1zeta). Qed. @@ -654,7 +654,7 @@ Let A0bridge0 : {in S1, forall zeta, bridge0 zeta \in 'CF(M, 'A0(M))}. Proof. by move=> zeta /Zbridge0/zchar_on/cfun_onS->. Qed. Let sS1S2' : {subset S1 <= [predC S2]}. -Proof. +Proof. by move=> _ /seqIndP[s /setDP[kHCs _] ->]; rewrite !inE mem_seqInd // inE kHCs. Qed. @@ -771,7 +771,7 @@ without loss Dpsi: tau1 coh_tau1 @zeta1 / psi = eta_col 0 - zeta1. rewrite Dade_vchar // zchar_split A0bridge0 //. by rewrite rpredB ?char_vchar ?prTIred_char ?irrWchar. apply: (addrI q%:R); transitivity '[psi]; last first. - rewrite Dade_isometry ?A0bridge0 // (cfnormBd (omuS1 _ _)) //. + rewrite Dade_isometry ?A0bridge0 // (cfnormBd (omuS1 _ _)) //. by rewrite cfnorm_prTIred n1S1. rewrite Dpsi [RHS]cfnormDd; last first. rewrite opprB cfdotC cfdot_sumr big1 ?conjC0 // => i _. @@ -827,7 +827,7 @@ have Rbeta: cfReal beta. rewrite /cfReal eq_sym -subr_eq0 rmorphD !rmorphB /= opprB 2!opprD opprB -/j. rewrite 2![(eta_ 0 _)^*%CF]cfAut_cycTIiso -!cycTIirr_aut !aut_Iirr0 -Dade_aut. set k := aut_Iirr conjC j; rewrite -(betaE 0 k) ?aut_Iirr_eq0 // addrACA. - rewrite addrC addr_eq0 addrCA subrK opprD opprK Dn raddfZnat -!raddfB /= -Dn. + rewrite addrC addr_eq0 addrCA subrK opprD opprK Dn raddfZnat -!raddfB /= -Dn. apply/eqP; rewrite (cfConjC_Dade_coherent coh_tau1) ?mFT_odd // -raddfB. rewrite Dtau1 ?Zzeta_S1 ?cfAut_seqInd //= -linearZ scalerBr; congr (tau _). rewrite opprD !rmorphB !deltaZ /= -!prTIirr_aut !aut_Iirr0 addrACA subrr. @@ -955,7 +955,7 @@ without loss tau2muj: tau2 coh_tau2 / tau2 (mu_ j) = eta_col j; last first. by case; apply/seqIndS/Iirr_kerDS; rewrite ?joing_subr. by rewrite !mem_seqInd // inE orbC inE kCi k'HUi andbT orbN. move: tau_theta; rewrite -tau2muj // -raddfZnat. - apply: (bridge_coherent scohM) sS20 coh_tau2 sS10 coh_tau1 sS1S2' _. + apply: (bridge_coherent scohM) sS20 coh_tau2 sS10 coh_tau1 sS1S2' _. by rewrite (cfun_onS _ HUtheta) ?setSD // rpredZnat ?Z_S1. move=> IHtau2; apply: (IHtau2 tau2 coh_tau2); have [IZtau2 Dtau2] := coh_tau2. have{IHtau2} /hasP[xi S2xi /=irr_xi]: has [mem irr M] S2. diff --git a/mathcomp/odd_order/PFsection12.v b/mathcomp/odd_order/PFsection12.v index fcc35bf..f605c0f 100644 --- a/mathcomp/odd_order/PFsection12.v +++ b/mathcomp/odd_order/PFsection12.v @@ -177,7 +177,7 @@ have nrS: ~~ has cfReal calS by apply: seqInd_notReal; rewrite ?mFT_odd. have U_S: uniq calS by apply: seqInd_uniq. have ccS: cfConjC_closed calS by apply: cfAut_seqInd. have conjCS: cfConjC_subset calS (seqIndD H L H 1) by split. -case: R1gen @R1 => /= R1 subc1. +case: R1gen @R1 => /= R1 subc1. have [[chi_char nrI ccI] tau_iso oI h1 hortho] := subc1. pose R chi := flatten [seq R1 'chi_i | i in S_ chi]. have memI phi i: phi \in calS -> i \in S_ phi -> 'chi_i \in calI. @@ -261,13 +261,13 @@ move=> notL1G_L2; without loss{notL1G_L2} disjointA1A: case: (Rgen _ _) @R1 => /= R1; set R1' := sval _ => [[subcoh1 hR1' defR1]]. case: (Rgen _ _) @R2 => /= R2; set R2' := sval _ => [[subcoh2 hR2' defR2]]. pose tau1 := FT_Dade maxL1; pose tau2 := FT_Dade maxL2. -move=> chi1 chi2 calS1_chi1 calS2_chi2. +move=> chi1 chi2 calS1_chi1 calS2_chi2. have [_ _ _ /(_ chi1 calS1_chi1)[Z_R1 o1R1 dtau1_chi1] _] := subcoh1. have{o1R1} [uR1 oR1] := orthonormalP o1R1. apply/orthogonalP=> a b R1a R2b; pose psi2 := tau2 (chi2 - chi2^*%CF). have Z1a: a \in dirr G by rewrite dirrE Z_R1 //= oR1 ?eqxx. suffices{b R2b}: '[a, psi2] == 0. - apply: contraTeq => nz_ab; rewrite /psi2 /tau2. + apply: contraTeq => nz_ab; rewrite /psi2 /tau2. have [_ _ _ /(_ chi2 calS2_chi2)[Z_R2 o1R2 ->] _] := subcoh2. suffices [e ->]: {e | a = if e then - b else b}. rewrite -scaler_sign cfdotC cfdotZr -cfdotZl scaler_sumr. @@ -338,7 +338,7 @@ Let S_ (chi : 'CF(L)) := [set i in irr_constt chi]. Lemma FTtype1_ortho_constant (psi : 'CF(G)) x : {in calS, forall phi, orthogonal psi (R phi)} -> x \in L :\: H -> {in x *: H, forall y, psi y = psi x}%g. -Proof. +Proof. move=> opsiR /setDP[Lx H'x]; pose Rpsi := 'Res[L] psi. have nsHL: H <| L := gFnormal _ _; have [sHL _] := andP nsHL. have [U [[[_ _ sdHU] [U1 inertU1] _] _]] := FTtypeP 1 maxL Ltype1. @@ -385,7 +385,7 @@ have {supp12B} oResD xi i1 i2 : xi \in calS -> i1 \in S_ xi -> i2 \in S_ xi -> apply/eqP; rewrite -subr_eq0; have := supp12B w; rewrite !cfunE => -> //. by rewrite tADH in_set0. have{nzAH} tiH: normedTI ('A(L) :\: H^#) G L by rewrite -A1Hdef TIsub ?A1Hdef. - have{supp12B} supp12B : 'chi_i1 - 'chi_i2 \in 'CF(L, 'A(L) :\: H^#). + have{supp12B} supp12B : 'chi_i1 - 'chi_i2 \in 'CF(L, 'A(L) :\: H^#). by apply/cfun_onP; apply: supp12B. have [_ /subsetIP[_ nAHL] _] := normedTI_P tiH. pose tau1 := restr_Dade ddL (subsetDl _ _) nAHL. @@ -412,7 +412,7 @@ move=> _ /lcosetP[h Hh ->] /=; rewrite (cfun_sum_cfdot Rpsi). pose calX := Iirr_kerD L H 1%g; rewrite (bigID (mem calX) xpredT) /= !cfunE. set sumX := \sum_(i in _) _; suffices HsumX: sumX \in 'CF(L, H). rewrite !(cfun_on0 HsumX) ?groupMr // !sum_cfunE. - rewrite !add0r; apply: eq_bigr => i;rewrite !inE sub1G andbT negbK => kerHi. + rewrite !add0r; apply: eq_bigr => i; rewrite !inE sub1G andbT negbK => kerHi. by rewrite !cfunE cfkerMr ?(subsetP kerHi). rewrite [sumX](set_partition_big _ (FTtype1_irr_partition L)) /=. apply: rpred_sum => A; rewrite inE => /mapP[xi calS_xi defA]. @@ -456,7 +456,7 @@ have tiP: trivIset P. case: ifP (cfclass_Ind_cases i1 i2 nsH'H) => _; first by rewrite /P_ => ->. have NiH i: 'Ind[H,H'] 'chi_i \is a character by rewrite cfInd_char ?irr_char. case/(constt_ortho_char (NiH i1) (NiH i2) i1Hj i2Hj)/eqP/idPn. - by rewrite cfnorm_irr oner_eq0. + by rewrite cfnorm_irr oner_eq0. have coverP: cover P =i predT. move=> j; apply/bigcupP; have [i jH'i] := constt_cfRes_irr H' j. by exists (P_ i); [apply: mem_imset | rewrite inE constt_Ind_Res]. @@ -524,7 +524,7 @@ have frobHU: [Frobenius L = H ><| U] := set_Frobenius_compl defL frobL. have [R [scohS _ _]] := Rgen maxL Ltype1; rewrite -/calS -/tau in scohS. have [tiH | [cHH _] | [expUdvH1 _]] := MtypeI. - have /Sibley_coherence := And3 (mFT_odd L) nilH tiH. - case/(_ U)=> [|tau1 [IZtau1 Dtau1]]; first by left. + case/(_ U)=> [|tau1 [IZtau1 Dtau1]]; first by left. exists tau1; split=> // chi Schi; rewrite Dtau1 //. by rewrite /tau Dade_Ind ?FTsupp_Frobenius ?(zcharD1_seqInd_on _ Schi). - apply/(uniform_degree_coherence scohS)/(@all_pred1_constant _ #|L : H|%:R). @@ -819,7 +819,7 @@ Let Ecyclic_le_p : cyclic E /\ (e %| p.-1) || (e %| p.+1). Proof. pose P := 'O_p(H)%G; pose T := 'Ohm_1('Z(P))%G. have sylP: p.-Sylow(H) P := nilpotent_pcore_Hall p (Fcore_nil L). -have [[sPH pP _] [sP0M pP0 _]] := (and3P sylP, and3P sylP0). +have [[sPH pP _] [sP0M pP0 _]] := (and3P sylP, and3P sylP0). have sP0P: P0 \subset P by rewrite (sub_normal_Hall sylP) ?pcore_normal. have defP0: P :&: M = P0. rewrite [P :&: M](sub_pHall sylP0 (pgroupS _ pP)) ?subsetIl ?subsetIr //. @@ -861,7 +861,7 @@ have ffulE: mx_faithful rE by apply: abelem_mx_faithful. have p'E: [char 'F_p]^'.-group E. rewrite (eq_p'group _ (charf_eq (char_Fp pr_p))) (coprime_p'group _ pV) //. by rewrite coprime_sym (coprimeSg sVH) ?(Frobenius_coprime frobHE). -have dimV: 'dim V = 2 by rewrite (dim_abelemE abelV) // oV pfactorK. +have dimV: 'dim V = 2 by rewrite (dim_abelemE abelV) // oV pfactorK. have cEE: abelian E. by rewrite dimV in (rE) ffulE; apply: charf'_GL2_abelian (mFT_odd E) ffulE _. have Enonscalar y: y \in E -> y != 1%g -> ~~ is_scalar_mx (rE y). @@ -986,7 +986,7 @@ have Sgt1: (1 < size calS)%N by apply: seqInd_nontrivial Schi; rewrite ?mFT_odd. have De: #|L : H| = e by rewrite -(index_sdprod defL). have [] := Dade_Ind1_sub_lin cohS_H Sgt1 irr_chi Schi; rewrite ?De //. rewrite -/tauL_H -/calS -/psi /=; set alpha := 'Ind 1 - chi. -case=> o_tau_1 tau_alpha_1 _ [Gamma [o_tau1_Ga _ [a Za tau_alpha] _] _]. +case=> o_tau_1 tau_alpha_1 _ [Gamma [o_tau1_Ga _ [a Za tau_alpha] _] _]. have [[Itau1 _] Dtau1] := cohS_H. have o1calS: orthonormal calS. by rewrite (sub_orthonormal irrS) ?seqInd_uniq ?irr_orthonormal. @@ -1227,7 +1227,7 @@ have{lb_psiM lb_psiL ub_rhoML ubM} ubK: (#|K / K'|%g < 4)%N. rewrite invfM invrK mulrC -(subrK #|K|%:R #|K'|%:R) mulrDl divff ?neq0CG //. rewrite -opprB mulNr addrC ltr_subr_addl -ltr_subr_addr. have /Frobenius_context[_ _ ntE _ _] := set_Frobenius_compl defL frobL. - have egt2: (2 < e)%N by rewrite odd_geq ?mFT_odd ?cardG_gt1. + have egt2: (2 < e)%N by rewrite odd_geq ?mFT_odd ?cardG_gt1. have e1_gt0: 0 < e.-1%:R :> algC by rewrite ltr0n -(subnKC egt2). apply: ltr_le_trans (_ : e%:R / e.-1%:R ^+ 2 <= _). rewrite ltr_pdivl_mulr ?exprn_gt0 //. @@ -1254,7 +1254,7 @@ have [/sdprodP[_ _ nKU0 tiKU0] ntK _ _ _] := Frobenius_context frobU0. have nK'U0: U0 \subset 'N(K') by apply: gFnorm_trans. have frobU0K': [Frobenius K <*> U0 / K' = (K / K') ><| (U0 / K')]%g. have solK: solvable K by rewrite ?nilpotent_sol ?Fcore_nil. - rewrite Frobenius_proper_quotient ?(sol_der1_proper solK) // /(_ <| _). + rewrite Frobenius_proper_quotient ?(sol_der1_proper solK) // /(_ <| _). by rewrite (subset_trans (der_sub 1 _)) ?joing_subl // join_subG gFnorm. have isoU0: U0 \isog U0 / K'. by rewrite quotient_isog //; apply/trivgP; rewrite -tiKU0 setSI ?gFsub. diff --git a/mathcomp/odd_order/PFsection13.v b/mathcomp/odd_order/PFsection13.v index 18e8606..339df0f 100644 --- a/mathcomp/odd_order/PFsection13.v +++ b/mathcomp/odd_order/PFsection13.v @@ -532,7 +532,7 @@ have Zalpha: alpha \in 'Z[irr H]. rewrite cfResInd_sum_cfclass ?reindex_cfclass -?cfnorm_Ind_irr //=. rewrite scalerK ?cfnorm_eq0 ?cfInd_eq0 ?irr_neq0 ?irr_char ?gFsub //. by apply: rpred_sum => i _; apply: irr_vchar. -have{Da_ Za_} Za: a \in Cint by rewrite -[a]Da_ ?Za_ ?sS1H. +have{Da_ Za_} Za: a \in Cint by rewrite -[a]Da_ ?Za_ ?sS1H. exists alpha => //; split=> //. set a1 := a / _ in Dchi; pose phi := a1 *: 'Res zeta1 + alpha. transitivity (#|H|%:R * '[phi] - `|phi 1%g| ^+ 2). @@ -738,7 +738,7 @@ have [tau1 cohS [b _ Dtau1]] := FTtypeP_coherence. have Zeta01: eta01 \in 'Z[irr G] by rewrite cycTIiso_vchar. pose j1 := signW2 b #1; pose d : algC := (-1) ^+ b; pose mu1 := mu_ j1. have nzj1: j1 != 0 by [rewrite signW2_eq0 ?Iirr1_neq0]; have S1mu1 := S1mu nzj1. -have o_mu_eta01 j: j != 0 -> '[tau1 (mu_ j), eta01] = d *+ (j == j1). +have o_mu_eta01 j: j != 0 -> '[tau1 (mu_ j), eta01] = d *+ (j == j1). move/Dtau1->; rewrite -/d cfdotZl cfdot_suml big_ord_recl /=. rewrite cfdot_cycTIiso andTb (inv_eq (signW2K b)). by rewrite big1 ?addr0 ?mulr_natr // => i _; rewrite cfdot_cycTIiso. @@ -783,7 +783,7 @@ have{tau1muj} ->: tau1 lambda x = sum_eta1 x. have Hmuj: mu_ j \in calH := Hmu nz_j. have dmu1: (lambda - mu_ j) 1%g == 0 by rewrite !cfunE !calHuq ?subrr. have H1dmu: lambda - mu_ j \in 'CF(S, H^#). - by rewrite cfun_onD1 rpredB ?((seqInd_on (gFnormal _ _)) setT). + by rewrite cfun_onD1 rpredB ?((seqInd_on (gFnormal _ _)) setT). have [_ ->] := cohS; last first. by rewrite zcharD1E ?rpredB ?mem_zchar ?FTseqInd_TIred /=. have A0dmu := cfun_onS (Fitting_sub_FTsupp0 maxS) H1dmu. @@ -968,8 +968,8 @@ Section Thirteen_10_to_13_15. Variable lambda : 'CF(S). Hypotheses (Slam : lambda \in calS) (irrHlam : irrIndH lambda). -Let Hlam : lambda \in calH. Proof. by have [] := andP irrHlam. Qed. -Let Ilam : lambda \in irr S. Proof. by have [] := andP irrHlam. Qed. +Let Hlam : lambda \in calH. Proof. by have [] := andP irrHlam. Qed. +Let Ilam : lambda \in irr S. Proof. by have [] := andP irrHlam. Qed. Let c := #|C|. Let u := #|U : C|. @@ -1045,7 +1045,7 @@ have Kdtheta xi: by rewrite cfInd_on ?subsetT. have oHK alpha beta: alpha \in 'CF(G, HG) -> beta \in 'CF(G, KG) -> '[alpha, beta] = 0. -- by move=> Halpha Kbeta; rewrite (cfdotElr Halpha Kbeta) tiHK big_set0 mulr0. +- by move=> Halpha Kbeta; rewrite (cfdotElr Halpha Kbeta) tiHK big_set0 mulr0. have o_lambda_theta: '[tau1S lambda, tau1T theta] = 0. pose S1 := lambda :: lambda^*%CF; pose T1 := theta :: theta^*%CF. have sS1S: {subset S1 <= calS} by apply/allP; rewrite /= Slam cfAut_seqInd. @@ -1118,7 +1118,7 @@ have{meanTI} meanG f : have{type24} tiK: normedTI K^# G T by have/type24[] := TtypeP. move=> fJ; rewrite -!meanTI // {1}/mean (big_setD1 1%g) // (big_setID H1G) /=. rewrite [in rhs in _ + (_ + rhs)](big_setID K1G) /= -/g -!mulrDl !addrA. - congr ((_ + _ + _ + _) / g); rewrite ?(setIidPr _) // /H1G /K1G. + congr ((_ + _ + _ + _) / g); rewrite ?(setIidPr _) // /H1G /K1G. + by rewrite class_supportEr -cover_imset -class_supportD1 setSD ?subsetT. + rewrite subsetD -setI_eq0 setIC tiHK eqxx andbT. by rewrite class_supportEr -cover_imset -class_supportD1 setSD ?subsetT. @@ -1126,7 +1126,7 @@ have{meanTI} meanG f : apply: eq_bigl => x; rewrite !inE andbT -!negb_or orbCA orbA orbC. by case: (x =P 1%g) => //= ->; rewrite mem_class_support ?group1. have lam1_ub: mean G0 G (nm2 lam1) <= lambda 1%g ^+ 2 / #|S|%:R - g^-1. - have [[Itau1 Ztau1] _] := cohS. + have [[Itau1 Ztau1] _] := cohS. have{Itau1} n1lam1: '[lam1] = 1 by rewrite Itau1 ?mem_zchar ?irrWnorm. have{Ztau1} Zlam1: lam1 \in 'Z[irr G] by rewrite Ztau1 ?mem_zchar. rewrite -ler_opp2 opprB -(ler_add2l '[lam1]) {1}n1lam1 addrCA. @@ -1452,7 +1452,7 @@ Lemma FTtypeP_primes_mod_cases : & p != 1 %[mod q] -> [/\ coprime ustar p.-1, ustar == 1 %[mod q] & forall b, b %| ustar -> b == 1 %[mod q]]]. -Proof. +Proof. have ustar_mod r: p = 1 %[mod r] -> ustar = q %[mod r]. move=> pr1; rewrite -[q]card_ord -sum1_card /ustar predn_exp //. rewrite -(subnKC pgt2) mulKn // subnKC //. @@ -1510,7 +1510,7 @@ have b_odd: odd b by rewrite Dbu odd_mul mFT_odd andbT in ustar_odd. case: ifPn => [/p1_q q_dv_ustar | /p'1_q[_ _ /(_ b)]]. have /dvdnP[c Db]: q %| b. rewrite Dbu Gauss_dvdl // coprime_sym in q_dv_ustar. - by apply: coprimeSg coPUq; have /mulG_sub[_ sUPU] := sdprodW defPU. + by apply: coprimeSg coPUq; have /mulG_sub[_ sUPU] := sdprodW defPU. have c_odd: odd c by rewrite Db odd_mul mFT_odd andbT in b_odd. suffices /eqP c1: c == 1%N by rewrite Dbu Db c1 mul1n mulKn ?prime_gt0. rewrite eqn_leq odd_gt0 // andbT -ltnS -(odd_ltn 3) // ltnS. @@ -1820,7 +1820,7 @@ have Dgamma: 'Ind[S, P <*> W1] 1 = (gamma %% P)%CF. by rewrite quotientYidl //; have [] := sdprodP defPW1. have gamma1: gamma 1%g = u%:R. rewrite -cfMod1 -Dgamma cfInd1 // cfun11 -divgS // -(sdprod_card defPW1). - by rewrite mulr1 -(sdprod_card defS) -(sdprod_card defPU) divnMr // mulKn. + by rewrite mulr1 -(sdprod_card defS) -(sdprod_card defPU) divnMr // mulKn. have frobUW1: [Frobenius U <*> W1 = U ><| W1] by have [[]] := Sfacts. have q_dv_u1: q %| u.-1 := Frobenius_dvd_ker1 frobUW1. have [nP_UW1 /isomP[/=]] := sdprod_isom defS_P; set h := restrm _ _ => injh hS. @@ -2041,7 +2041,7 @@ have ZsubL psi: psi \in calL -> psi - psi^*%CF \in 'Z[calL, L^#]. have mem_eta j: eta_ 0 j \in map sigma (irr W) by rewrite map_f ?mem_irr. have otau1eta: orthogonal (map tau1 calL) (map sigma (irr W)). apply/orthogonalP=> _ _ /mapP[psi Lpsi ->] /mapP[w irr_w ->]. - have{w irr_w} [i [j ->]] := cycTIirrP defW irr_w; rewrite -/(w_ i j). + have{w irr_w} [i [j ->]] := cycTIirrP defW irr_w; rewrite -/(w_ i j). pose Psi := tau1 (psi - psi^*%CF); pose NC := cyclicTI_NC ctiWG. have [[Itau1 Ztau1] Dtau1] := cohL. have Lpsis: psi^*%CF \in calL by rewrite cfAut_seqInd. @@ -2114,7 +2114,7 @@ have{Gamma_even} odd_bSphi_bLeta: (bSphi + bLeta == 1 %[mod 2])%C. rewrite 2!cfdotDl 2!['[_, eta01]]cfdotDl 2!['[_, Gamma]]cfdotDl !cfdotNl. rewrite cfnorm1 o_GaL_1 ['[1, Gamma]]cfdotC Ga1 conjC0 addr0 add0r. have ->: 1 = eta_ 0 0 by rewrite /w_ cycTIirr00 cycTIiso1. - rewrite cfdot_cycTIiso mulrb ifN_eqC ?Iirr1_neq0 // add0r. + rewrite cfdot_cycTIiso mulrb ifN_eqC ?Iirr1_neq0 // add0r. rewrite 2?(orthogonalP otau1eta _ _ (map_f _ _) (mem_eta _)) // oppr0 !add0r. by rewrite addr0 addrA addrC addr_eq0 !opprB addrA /eqCmod => /eqP <-. have abs_mod2 a: a \in Cint -> {b : bool | a == b%:R %[mod 2]}%C. diff --git a/mathcomp/odd_order/PFsection14.v b/mathcomp/odd_order/PFsection14.v index bed35bc..1b8a531 100644 --- a/mathcomp/odd_order/PFsection14.v +++ b/mathcomp/odd_order/PFsection14.v @@ -231,7 +231,7 @@ have lb_b ij (b_ij := b (sigma 'chi_ij)): 1 <= `|b_ij| ^+ 2 ?= iff [exists n : bool, b_ij == (-1) ^+ n]. - have /codomP[[i j] Dij] := dprod_Iirr_onto defW ij. have{b_ij} ->: b_ij = a i j. - rewrite /a /w_ -Dij Dbeta defGa 2!cfdotDl. + rewrite /a /w_ -Dij Dbeta defGa 2!cfdotDl. have ->: '[X, sigma 'chi_ij] = b_ij by rewrite /b_ij Db. by rewrite (orthoPl oYeta) ?(orthoPl oZeta) ?map_f ?mem_irr // !addr0. have Zaij: a i j \in Cint by rewrite Cint_cfdot_vchar ?cycTIiso_vchar. @@ -282,7 +282,7 @@ suffices /cfdot_add_dirr_eq1: '[tau1L phi - tau1L phi^*%CF, chi] = 1. rewrite cfdotBr (span_orthogonal o_tauLeta) ?add0r //; last first. by rewrite rpredB ?memv_span ?map_f ?cfAut_seqInd. have Zdphi := seqInd_sub_aut_zchar nsHL conjC Lphi. -rewrite -raddfB Dtau1 ?zcharD1_seqInd // Dade_isometry ?(zchar_on Zdphi) //. +rewrite -raddfB Dtau1 ?zcharD1_seqInd // Dade_isometry ?(zchar_on Zdphi) //. rewrite cfdotBr !cfdotBl cfdot_conjCl cfAutInd rmorph1 irrWnorm //. rewrite (seqInd_ortho_Ind1 _ _ Lphi) // conjC0 subrr add0r opprK. by rewrite cfdot_conjCl (seqInd_conjC_ortho _ _ _ Lphi) ?mFT_odd ?conjC0 ?subr0. @@ -596,7 +596,7 @@ have /exists_inP[x /setD1P[ntx R0x] ntCPx]: [exists x in R0^#, 'C_P[x] != 1%g]. by rewrite gen_subG; apply/bigcupsP=> x /(eqfun_inP regR0P)->. have{x ntx R0x ntCPx} sZR_R0: 'Z(R) \subset R0. have A0x: x \in 'A0(S). - have [z /setIP[Pz cyz] ntz] := trivgPn _ ntCPx. + have [z /setIP[Pz cyz] ntz] := trivgPn _ ntCPx. apply/setUP; left; apply/bigcupP; exists z. by rewrite !inE ntz (subsetP (Fcore_sub_FTcore maxS)). by rewrite (eqP Stype2) 3!inE ntx cent1C (subsetP sUPU) ?(subsetP sR0U). @@ -798,7 +798,7 @@ have nzT1_Ga zeta: zeta \in calT1 -> `|'[Gamma, tau1T zeta]| ^+ 2 >= 1. have A0betaT0: betaT0 \in 'CF(T, 'A0(T)). by rewrite (cfun_onS (FTsupp1_sub0 _)) // /'A1(T) ?FTcore_eq_der1. have ZbetaT0: betaT0 \in 'Z[irr T]. - by rewrite rpredB ?char_vchar ?(seqInd_char T1zeta) ?prTIred_char. + by rewrite rpredB ?char_vchar ?(seqInd_char T1zeta) ?prTIred_char. pose Delta := tauT betaT0 - 1 + tau1T zeta. have nz_i1: #1 != 0 := Iirr1_neq0 ntW2. rewrite -(canLR (addKr _) (erefl Delta)) opprB cfdotDr cfdotBr oGa1 add0r. diff --git a/mathcomp/odd_order/PFsection2.v b/mathcomp/odd_order/PFsection2.v index f92bb16..c982642 100644 --- a/mathcomp/odd_order/PFsection2.v +++ b/mathcomp/odd_order/PFsection2.v @@ -315,7 +315,7 @@ Section AutomorphismCFun. Variable u : {rmorphism algC -> algC}. Local Notation "alpha ^u" := (cfAut u alpha). -Lemma Dade_aut alpha : (alpha^u)^\tau = (alpha^\tau)^u. +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). @@ -325,7 +325,7 @@ Qed. End AutomorphismCFun. -Lemma Dade_conjC alpha : (alpha^*)^\tau = ((alpha^\tau)^*)%CF. +Lemma Dade_conjC alpha : (alpha^*)^\tau = ((alpha^\tau)^*)%CF. Proof. exact: Dade_aut. Qed. (* This is Peterfalvi (2.7), main part *) @@ -344,7 +344,7 @@ 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 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. @@ -507,7 +507,7 @@ have defMBx: 'M(B :^ x) = 'M(B) :^ x. 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. + 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 //=. @@ -542,7 +542,7 @@ 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). +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. @@ -551,7 +551,7 @@ 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. +- 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. @@ -559,7 +559,7 @@ have supp_aBgP: {in calA g 'M(B), forall x, 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. + 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. @@ -571,7 +571,7 @@ have supp_aBgP: {in calA g 'M(B), forall x, 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. + 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. @@ -697,7 +697,7 @@ 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. + 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=> _ ->. diff --git a/mathcomp/odd_order/PFsection3.v b/mathcomp/odd_order/PFsection3.v index eb5ccf8..6bff279 100644 --- a/mathcomp/odd_order/PFsection3.v +++ b/mathcomp/odd_order/PFsection3.v @@ -715,7 +715,7 @@ Proof. by move=> sth21 Uth1 m /(sat_exact sth21)/Uth1. Qed. Fact tr_Lmodel_subproof (m : model) : is_Lmodel (tr m) (fun ij => m (tr ij)). Proof. case: m => /= d f _ [[odd_d1 odd_d2 d1gt1 d2gt1 neq_d12] Zf fP] _. -split=> // [|[j1 i1] [j2 i2]]; first by rewrite eq_sym. +split=> // [|[j1 i1] [j2 i2]]; first by rewrite eq_sym. by rewrite ![_ \in _]andbC /= => wf_ij1 wf_ij2; rewrite fP // /dot_ref mulnC. Qed. @@ -1079,7 +1079,7 @@ rewrite -[f in f _ kvs2]/(idfun _); set f := idfun _; rewrite /= in f *. have [/= _ Ukvs2 kvsP] := satP m_th _ th_cl2. move: Ukvs2; set kvs2' := kvs2; set mm := false. have /allP: {subset kvs2' <= kvs2} by []. -pose lit12 k := (k, 1) \in kvs1 /\ (k, 1) \in kvs2. +pose lit12 k := (k, 1) \in kvs1 /\ (k, 1) \in kvs2. have: mm -> {k | lit12 k & k \notin unzip1 kvs2'} by []. elim: kvs2' mm => [|[k v2] kvs2' IH] //= mm mmP /andP[kvs2k /IH{IH}IHkvs]. case/andP=> kvs2'k /IHkvs{IHkvs}IHkvs; case: ifP => [_ | /norP[]]. @@ -1087,7 +1087,7 @@ case/andP=> kvs2'k /IHkvs{IHkvs}IHkvs; case: ifP => [_ | /norP[]]. have [v1 /= kvs1k | //] := get_litP; case: eqP => // -> in kvs2k * => _ nz_v1. case Dbb: (th_bbox th) (th_bboxP (bbox_refl (th_bbox th))) => [ri rj] rijP. have [/andP[/=lti1r ltj1r] /andP[/=lti2r _]] := (rijP _ th_cl1, rijP _ th_cl2). -have rkP := th_dimP (leqnn _) _ th_cl1; have /= ltkr := rkP _ kvs1k. +have rkP := th_dimP (leqnn _) _ th_cl1; have /= ltkr := rkP _ kvs1k. have symP := unsat_match (Sym [:: i2; i1] [:: j1] _) _ _ m m_th. rewrite /= Dbb lti1r lti2r ltj1r inE eq_sym neq_i /= in symP. have [Dv1 | v1_neq1] /= := altP eqP; first rewrite Dv1 in kvs1k. @@ -1156,7 +1156,7 @@ consider b42; uwlog Db42: (& b42 = x6 - x4 + x5). by uhave -x2 in b42 as O(42, 31); symmetric to b42x4. by uhave ~x1 in b42 as L(42, 41); uhave x5 in b42 as O(42, 21); uexact Db42. uwlog Db32: (& ? in b32); first uexact Db32. -uwlog Db41: (& ? in b41); first uexact Db41. +uwlog Db41: (& ? in b41); first uexact Db41. consider b12; uwlog b12x5: x5 | ~x5 in b12 as L(12, 42). uhave ~x6 | x6 in b12 as L(12, 42); last by consider b22; symmetric to b12x5. uhave -x4 in b12 as O(12, 42); uhave x1 in b12 as O(12, 21). @@ -1521,7 +1521,7 @@ Lemma cycTI_NC_opp (phi : 'CF(G)) : (NC (- phi)%R = NC phi)%N. Proof. by apply: eq_card=> [[i j]]; rewrite !inE cfdotNl oppr_eq0. Qed. Lemma cycTI_NC_sign (phi : 'CF(G)) n : (NC ((-1) ^+ n *: phi)%R = NC phi)%N. -Proof. +Proof. elim: n=> [|n IH]; rewrite ?(expr0,scale1r) //. by rewrite exprS -scalerA scaleN1r cycTI_NC_opp. Qed. @@ -1561,7 +1561,7 @@ Qed. Lemma cycTI_NC_sub n1 n2 phi1 phi2 : (NC phi1 <= n1 -> NC phi2 <= n2 -> NC (phi1 - phi2)%R <= n1 + n2)%N. -Proof. by move=> ub1 ub2; rewrite cycTI_NC_add ?cycTI_NC_opp. Qed. +Proof. by move=> ub1 ub2; rewrite cycTI_NC_add ?cycTI_NC_opp. Qed. Lemma cycTI_NC_scale_nz a phi : a != 0 -> NC (a *: phi) = NC phi. Proof. @@ -1660,7 +1660,7 @@ Lemma cycTI_NC_minn (phi : 'CF(G)) : (minn w1 w2 <= NC phi)%N. Proof. move=> phiV_0 /andP[/card_gt0P[[i0 j0]]]; rewrite inE /= => nz_a0 ubNC. -pose L := [seq (i0, j) | j : Iirr W2]; pose C := [seq (i, j0) | i : Iirr W1]. +pose L := [seq (i0, j) | j : Iirr W2]; pose C := [seq (i, j0) | i : Iirr W1]. have [oL oC]: #|L| = w2 /\ #|C| = w1 by rewrite !card_image // => i j []. have [Da | Da] := small_cycTI_NC phiV_0 ubNC nz_a0. rewrite geq_min -oC subset_leq_card //. @@ -1726,7 +1726,7 @@ have NCk2'_le1 (dI : {set _}): - rewrite (cardsD1 dk2) => -> /eqP/cards1P[dk ->]. by rewrite big_set1 cycTI_NC_dirr ?dirr_dchi. suffices /psi_phi'_lt0/ltr_geF/idP[]: dk2 \in Irho :\: Iphi. - rewrite rhoIdE cfdotZr signrN rmorphN mulNr oppr_ge0 rmorph_sign. + rewrite rhoIdE cfdotZr signrN rmorphN mulNr oppr_ge0 rmorph_sign. have := small_cycTI_NC psiV0 NCpsi psi_k1_neq0. by case=> // ->; rewrite mulrCA nmulr_lle0 ?ler0n. have: (1 + 1 < NC psi)%N. diff --git a/mathcomp/odd_order/PFsection4.v b/mathcomp/odd_order/PFsection4.v index c897e84..b5f9344 100644 --- a/mathcomp/odd_order/PFsection4.v +++ b/mathcomp/odd_order/PFsection4.v @@ -482,7 +482,7 @@ Lemma prTIred_inj : injective mu_. Proof. move=> j1 j2 /(congr1 (cfdot (mu_ j1)))/esym/eqP; rewrite !cfdot_prTIred. by rewrite eqC_nat eqn_pmul2r ?cardG_gt0 // eqxx; case: (j1 =P j2). -Qed. +Qed. Lemma prTIred_not_real j : j != 0 -> ~~ cfReal (mu_ j). Proof. @@ -645,7 +645,7 @@ have [[_ nKL] [nKz _]] := (andP nsKL, setIdP Itheta_z). suffices{k theta Itheta_z} /eqP->: imIchi == 'Fix_Jirr[z]. by apply/afix1P/irr_inj; rewrite conjg_IirrE inertiaJ. rewrite eqEcard; apply/andP; split. - apply/subsetP=> _ /imsetP[j _ ->]; apply/afix1P/irr_inj. + apply/subsetP=> _ /imsetP[j _ ->]; apply/afix1P/irr_inj. by rewrite conjg_IirrE -(cfRes_prTIirr 0) (cfConjgRes _ _ nsKL) ?cfConjg_id. have ->: #|imIchi| = w2 by rewrite card_imset //; apply: prTIres_inj. have actsL_KK: [acts L, on classes K | 'Js \ subsetT L]. @@ -720,7 +720,7 @@ Record prime_Dade_hypothesis : Prop := PrimeDadeHypothesis { Hypothesis prDadeHyp : prime_Dade_hypothesis. Let ctiWG : cyclicTI_hypothesis G defW := prDadeHyp. -Let ptiWL : primeTI_hypothesis L K defW := prDadeHyp. +Let ptiWL : primeTI_hypothesis L K defW := prDadeHyp. Let ctiWL : cyclicTI_hypothesis L defW := prime_cycTIhyp ptiWL. Let ddA0 : Dade_hypothesis G L A0 := prDadeHyp. Local Notation ddA0def := (prDade_def prDadeHyp). @@ -838,7 +838,7 @@ Qed. (* First part of PeterFalvi (4.8). *) Lemma prDade_sub_TIirr_on i j k : j != 0 -> k != 0 -> mu2_ i j 1%g = mu2_ i k 1%g -> - mu2_ i j - mu2_ i k \in 'CF(L, A0). + mu2_ i j - mu2_ i k \in 'CF(L, A0). Proof. move=> nzj nzk eq_mu1. apply/cfun_onP=> g; rewrite defA0 !inE negb_or !cfunE => /andP[A'g V'g]. @@ -846,7 +846,7 @@ have [Lg | L'g] := boolP (g \in L); last by rewrite !cfun0 ?subrr. have{Lg} /bigcupP[_ /rcosetsP[x W1x ->] Kx_g]: g \in cover (rcosets K W1). by rewrite (cover_partition (rcosets_partition_mul W1 K)) (sdprodW defL). have [x1 | ntx] := eqVneq x 1%g. - have [-> | ntg] := eqVneq g 1%g; first by rewrite eq_mu1 subrr. + have [-> | ntg] := eqVneq g 1%g; first by rewrite eq_mu1 subrr. have{A'g} A1'g: g \notin 1%g |: A by rewrite !inE negb_or ntg. rewrite x1 mulg1 in Kx_g; rewrite -!(cfResE (mu2_ i _) sKL) ?cfRes_prTIirr //. by rewrite !(cfun_onP (prDade_TIres_on _)) ?subrr. @@ -924,7 +924,7 @@ have ccT: cfConjC_closed calT. by rewrite prTIred_aut cfunE conj_Cnat ?Cnat_char1 ?prTIred_char. have TonA: 'Z[calT, L^#] =i 'Z[calT, A]. have A'1: 1%g \notin A by apply: contra (subsetP sAA0 _) _; have [] := ddA0. - move => psi; rewrite zcharD1E -(setU1K A'1) zcharD1; congr (_ && _). + move=> psi; rewrite zcharD1E -(setU1K A'1) zcharD1; congr (_ && _). apply/idP/idP; [apply: zchar_trans_on psi => psi Tpsi | exact: zcharW]. have [j /andP[nz_j _] Dpsi] := imageP Tpsi. by rewrite zchar_split mem_zchar // Dpsi prDade_TIred_on. diff --git a/mathcomp/odd_order/PFsection5.v b/mathcomp/odd_order/PFsection5.v index 636c48c..e42e104 100644 --- a/mathcomp/odd_order/PFsection5.v +++ b/mathcomp/odd_order/PFsection5.v @@ -105,7 +105,7 @@ Lemma Iirr_kerDS A1 A2 B1 B2 : A2 \subset A1 -> B1 \subset B2 -> Iirr_kerD B1 A1 \subset Iirr_kerD B2 A2. Proof. by move=> sA12 sB21; rewrite setDSS ?Iirr_kerS. Qed. -Lemma Iirr_kerDY B A : Iirr_kerD (A <*> B) A = Iirr_kerD B A. +Lemma Iirr_kerDY B A : Iirr_kerD (A <*> B) A = Iirr_kerD B A. Proof. by apply/setP=> i; rewrite !inE join_subG; apply: andb_id2r => ->. Qed. Lemma mem_Iirr_ker1 i : (i \in Iirr_kerD K 1%g) = (i != 0). @@ -567,7 +567,7 @@ Lemma coherent_seqInd_conjCirr S tau R nu r : chi - chi^*%CF \in 'Z[S, L^#] & (nu chi - nu chi^*)%CF 1%g == 0]. Proof. move=> [[charS nrS ccS] [_ Ztau] oSS _ _] [[Inu Znu] Dnu] chi chi2 Schi. -have sSZ: {subset S <= 'Z[S]} by apply: mem_zchar. +have sSZ: {subset S <= 'Z[S]} by apply: mem_zchar. have vcharS: {subset S <= 'Z[irr L]} by move=> phi /charS/char_vchar. have Schi2: {subset chi2 <= 'Z[S]} by apply/allP; rewrite /= !sSZ ?ccS. have Schi_diff: chi - chi^*%CF \in 'Z[S, L^#]. @@ -608,7 +608,7 @@ have sS_ZS1: {subset S <= 'Z[S1]}; last apply: (subgen_coherent sS_ZS1). apply/allP=> eta Seta; rewrite -(rpredBr eta (rpredMn (a eta) Zeta1)). exact/mem_zchar/mem_behead/map_f. have{sS_ZS1} freeS1: free S1. - have Sgt0: (0 < size S)%N by case: (S) Seta1. + have Sgt0: (0 < size S)%N by case: (S) Seta1. rewrite /free eqn_leq dim_span /= size_map size_rem ?prednK // -(eqnP freeS). by apply/dimvS/span_subvP => eta /sS_ZS1/zchar_span. pose iso_eta1 zeta := zeta \in 'Z[S, L^#] /\ '[tau zeta, zeta1] = '[zeta, eta1]. @@ -650,7 +650,7 @@ pose beta chi := tau (chi - chi^*%CF); pose eqBP := _ =P beta _. have Zbeta: {in S, forall chi, chi - (chi^*)%CF \in 'Z[S, L^#]}. move=> chi Schi; rewrite /= zcharD1E rpredB ?mem_zchar ?ccS //= !cfunE. by rewrite subr_eq0 conj_Cnat // Cnat_char1 ?N_S. -pose sum_beta chi R := \sum_(alpha <- R) alpha == beta chi. +pose sum_beta chi R := \sum_(alpha <- R) alpha == beta chi. pose Zortho R := all (mem 'Z[irr G]) R && orthonormal R. have R chi: {R : 2.-tuple 'CF(G) | (chi \in S) ==> sum_beta chi R && Zortho R}. apply: sigW; case Schi: (chi \in S) => /=; last by exists [tuple 0; 0]. @@ -1153,7 +1153,7 @@ have Zachi: chi - a *: xi1 \in 'Z[S, L^#]. by rewrite zcharD1E !cfunE -chi1 subrr rpredB ?scale_zchar ?mem_zchar /=. have Ztau_achi := zcharW (Ztau _ Zachi). have [X R_X [Y defXY]] := subcoherent_split Schi Ztau_achi. -have [eqXY oXY oYRchi] := defXY; pose X1 := map tau1 (in_tuple S1). +have [eqXY oXY oYRchi] := defXY; pose X1 := map tau1 (in_tuple S1). suffices defY: Y = a *: tau1 xi1. by move: eqXY; rewrite defY; apply: extend_coherent_with; rewrite -?defY. have oX1: pairwise_orthogonal X1 by apply: map_pairwise_orthogonal. @@ -1321,7 +1321,7 @@ have [X [RchiX nX defX] XD_N]: exists2 X, Xspec X & XDspec X. suffices: '[X - X'] == 0 by rewrite cfnorm_eq0 subr_eq0 => /eqP->. have ZXX': '[X, X'] \in Cint by rewrite Cint_cfdot_vchar ?(zchar_trans ZRchi). rewrite cfnormB subr_eq0 nX nX' aut_Cint {ZXX'}//; apply/eqP/esym. - congr (_ *+ 2); rewrite -(addNKr (X - D xi1) X) cfdotDl cfdotC. + congr (_ *+ 2); rewrite -(addNKr (X - D xi1) X) cfdotDl cfdotC. rewrite (span_orthogonal (oR chi1 xi1 _ _)) // conjC0. rewrite -(subrK (D xi) X') cfdotDr cfdotDl cfdotNl opprB subrK. rewrite (span_orthogonal (oR xi1 xi _ _)) //; last exact/and3P. @@ -1358,7 +1358,7 @@ pose S1 := undup (phi1 :: phi1^* :: phi2 :: phi2^*)%CF. have sS1S: cfConjC_subset S1 S. split=> [|chi|chi]; rewrite ?undup_uniq //= !mem_undup; move: chi; apply/allP. by rewrite /= !ccS ?Sphi1 ?Sphi2. - by rewrite /= !inE !cfConjCK !eqxx !orbT. + by rewrite /= !inE !cfConjCK !eqxx !orbT. exists S1; rewrite !mem_undup !inE !eqxx !orbT; split=> //. apply: uniform_degree_coherence (subset_subcoherent scohS sS1S) _. apply/(@all_pred1_constant _ (phi2 1%g))/allP=> _ /mapP[chi S1chi ->] /=. diff --git a/mathcomp/odd_order/PFsection6.v b/mathcomp/odd_order/PFsection6.v index b32a57d..2add4af 100644 --- a/mathcomp/odd_order/PFsection6.v +++ b/mathcomp/odd_order/PFsection6.v @@ -14,7 +14,7 @@ Require Import sylow abelian maximal hall frobenius. From mathcomp Require Import matrix mxalgebra mxrepresentation vector ssrnum algC algnum. From mathcomp -Require Import classfun character inertia vcharacter integral_char. +Require Import classfun character inertia vcharacter integral_char. From mathcomp Require Import PFsection1 PFsection2 PFsection3 PFsection4 PFsection5. @@ -187,7 +187,7 @@ have{odd_e} mod1e_lb m: odd m -> m == 1 %[mod e] -> (m > 1 -> 2 * e + 1 <= m)%N. move=> odd_m e_dv_m1 m_gt1; rewrite eqn_mod_dvd 1?ltnW // subn1 in e_dv_m1. by rewrite mul2n addn1 dvdn_double_ltn. have nsH1L: H1 <| L by rewrite normalY // gFnormal_trans. -have nsH1K: H1 <| K by rewrite (normalS _ sKL nsH1L) // join_subG der_sub. +have nsH1K: H1 <| K by rewrite (normalS _ sKL nsH1L) // join_subG der_sub. have [sH1K nH1K] := andP nsH1K; have sMH1: M \subset H1 by apply: joing_subr. have cohH1: coherent (S H1) L^# tau. apply: uniform_degree_coherence (subset_subcoherent scohS _) _ => //. @@ -229,7 +229,7 @@ have not_abKb: ~~ abelian (K / M). by rewrite join_subG subxx andbT -quotient_der ?quotient_sub1. have /is_abelemP[p p_pr /and3P[pKb _ _]]: is_abelem (K / H1). have: solvable (K / H1)%g by apply: quotient_sol solK. - by case/(minnormal_solvable (chief_factor_minnormal chiefH1)). + by case/(minnormal_solvable (chief_factor_minnormal chiefH1)). have [[_ p_dv_Kb _] nsMK] := (pgroup_pdiv pKb ntKb, normalS sMK sKL nsML). have isoKb: K / M / (H1 / M) \isog K / H1 := third_isog sMH1 nsMK nsH1K. have{nilKM} pKM: p.-group (K / M)%g. @@ -309,7 +309,7 @@ have Ndg: {in calX, forall xi : 'CF(L), xi 1%g = (e * p ^ d xi)%:R}. rewrite /d => _ /seqIndP[i _ ->]; rewrite cfInd1 // -/e. have:= dvd_irr1_cardG i; have /CnatP[n ->] := Cnat_irr1 i. rewrite -natrM natCK dvdC_nat mulKn // -p_part => dv_n_K. - by rewrite part_pnat_id // (pnat_dvd dv_n_K). + by rewrite part_pnat_id // (pnat_dvd dv_n_K). have [chi Ychi leYchi]: {chi | chi \in Y & {in Y, forall xi, d xi <= d chi}%N}. have [/eqP/nilP Y0 | ntY] := posnP (size Y); first by rewrite Y0 in homoY. pose i := [arg max_(i > Ordinal ntY) d Y`_i]. @@ -459,7 +459,7 @@ suffices Ea2 l (phi := 'chi[G]_l) (kerZphi : kerZ l): - move=> l phi kerZphi. have Zphi1: phi 1%g \in Cint by rewrite irr1_degree rpred_nat. have chi0 x: x \in Z -> 'chi[G]_0 x = 1. - by rewrite irr0 cfun1E => /(subsetP sZG) ->. + by rewrite irr0 cfun1E => /(subsetP sZG) ->. have: kerZ 0 by move=> x y /setD1P[_ Zx] /setD1P[_ Zy]; rewrite !chi0. move/Ea2/(eqAmodMl (Aint_irr l z)); rewrite !{}chi0 // -/phi eqAmod_sym. rewrite mulrDr mulr1 !mulr_natr => /eqAmod_trans/(_ (Ea2 l kerZphi)). @@ -474,7 +474,7 @@ suffices Ea2 l (phi := 'chi[G]_l) (kerZphi : kerZ l): have: '['Res[Z] phi, 'chi_0] \in Crat. by rewrite rpred_Cnat ?Cnat_cfdot_char ?cfRes_char ?irr_char. rewrite irr0 cfdotE (big_setD1 _ (group1 Z)) cfun1E cfResE ?group1 //=. - rewrite rmorph1 mulr1; congr (_ * (_ + _) \in Crat). + rewrite rmorph1 mulr1; congr (_ * (_ + _) \in Crat). rewrite -sumr_const; apply: eq_bigr => x Z1x; have [_ Zx] := setD1P Z1x. by rewrite cfun1E cfResE ?Zx // rmorph1 mulr1; apply: kerZphi. pose alpha := 'omega_l['K_i1]; pose phi1 := phi 1%g. @@ -653,7 +653,7 @@ without loss [/p_groupP[p p_pr pH] not_cHH]: / p_group H /\ ~~ abelian H. by apply; rewrite (isog_abelian isoH) (pgroup_p pH). have sylH: p.-Sylow(G) H. (* required for (6.7) *) rewrite -Sylow_subnorm -normD1; have [_ _ /eqP->] := and3P tiA. - by apply/and3P; rewrite -oW1 -pgroupE (coprime_p'group _ pH) // coprime_sym. + by apply/and3P; rewrite -oW1 -pgroupE (coprime_p'group _ pH) // coprime_sym. pose caseA := 'Z(H) :&: W2 \subset [1]%g; pose caseB := ~~ caseA. have caseB_P: caseB -> [/\ case_c2, W2 :!=: 1%g & W2 \subset 'Z(H)]. rewrite /caseB /caseA; have [->|] := eqP; first by rewrite subsetIr. @@ -779,7 +779,7 @@ have{odd_frobL1} caseA_cohXY: caseA -> coherent (X ++ Y) L^# tau. pose psi1 := xi1 - a *: eta1. have Zpsi1: psi1 \in 'Z[S, L^#]. rewrite zcharD1E !cfunE (uniY _ Yeta1) -xi1_1 subrr eqxx andbT. - by rewrite rpredB ?rpredZ_Cnat ?mem_zchar ?(sXS _ Xxi1) // sYS. + by rewrite rpredB ?rpredZ_Cnat ?mem_zchar ?(sXS _ Xxi1) // sYS. have [Y1 dY1 [X1 [dX1 _ oX1tauY]]] := orthogonal_split (map tau1 Y)(tau psi1). have{dX1 Y1 dY1 oYtau} [b Zb tau_psi1]: {b | b \in Cint & tau psi1 = X1 - a *: tau1 eta1 + b *: (\sum_(eta <- Y) tau1 eta)}. @@ -896,7 +896,7 @@ have{odd_frobL1} caseA_cohXY: caseA -> coherent (X ++ Y) L^# tau. have [|//]:= leq_size_perm uYeta _ szY2. by apply/allP; rewrite /= Yeta1 ccY. have memYtau1c: {subset [seq tau1 eta^* | eta <- Y]%CF <= map tau1 Y}. - by move=> _ /mapP[eta Yeta ->]; rewrite /= map_f ?ccY. + by move=> _ /mapP[eta Yeta ->]; rewrite /= map_f ?ccY. apply: IH (dual_coherence scohY cohY szY2) _ _ _. - rewrite (map_comp -%R) orthogonal_oppr. by apply/orthogonalP=> phi psi ? /memYtau1c; apply: (orthogonalP o_tauXY). @@ -1188,7 +1188,7 @@ have{caseA_cohXY Itau1 Ztau1 Dtau1 oYYt} cohXY: coherent (X ++ Y) L^# tau. exists (YZ1 + b *: Y1) => [/oRY-oRiY|]; last first. by rewrite addrCA subrK addrC cfdotDl cfdotZl normY1 mulr1 addrN. apply/orthoPl=> aa Raa; rewrite cfdotDl (orthoPl oYZ1R) // add0r. - by rewrite cfdotC (span_orthogonal oRiY) ?conjC0 ?rpredZ // memv_span. + by rewrite cfdotC (span_orthogonal oRiY) ?conjC0 ?rpredZ // memv_span. case/all_and2=> defXbZ oZY1; have spanR_X1 := zchar_span (R_X1 _ _). have ub_alpha i: i \in rp -> [/\ '[chi i] <= '[X1 i] @@ -1214,7 +1214,7 @@ have{caseA_cohXY Itau1 Ztau1 Dtau1 oYYt} cohXY: coherent (X ++ Y) L^# tau. rewrite -(@ler_pexpn2r _ 2) ?qualifE ?(ltrW ai_gt0) ?norm_ger0 //. apply: ler_trans (_ : '[b i *: Y1 - Z1 i] <= _). rewrite cfnormBd; last by rewrite cfdotZl cfdotC oZY1 ?conjC0 ?mulr0. - by rewrite cfnormZ normY1 mulr1 ler_addl cfnorm_ge0. + by rewrite cfnormZ normY1 mulr1 ler_addl cfnorm_ge0. rewrite -(ler_add2l '[X1 i]) -cfnormBd; last first. rewrite cfdotBr cfdotZr (span_orthogonal (oRY i _)) ?spanR_X1 //. rewrite mulr0 sub0r cfdotC. diff --git a/mathcomp/odd_order/PFsection7.v b/mathcomp/odd_order/PFsection7.v index 455681c..deb1698 100644 --- a/mathcomp/odd_order/PFsection7.v +++ b/mathcomp/odd_order/PFsection7.v @@ -66,7 +66,7 @@ rewrite (DadeJ ddA) // cardJg; congr (_ * _). rewrite big_imset /= => [|z y0 _ _ /=]; last exact: conjg_inj. by apply: eq_bigr => u Hu; rewrite -conjMg cfunJ // (subsetP sLG). Qed. -Definition invDade alpha := Cfun 1 (invDade_subproof alpha). +Definition invDade alpha := Cfun 1 (invDade_subproof alpha). Local Notation "alpha ^\rho" := (invDade alpha). @@ -426,7 +426,7 @@ split=> // [ | chi /irrP[t def_chi] o_chiSnu]. have hu: h * u = e^-1 * (h - 1) by rewrite mulrCA (mulrBr h) mulr1 divff. have ->: '[(nu zeta)^\rho] = u * a ^+ 2 - v * a *+ 2 + w. have defT1: perm_eq calT [:: phi, Ind1H, zeta & S2]. - by rewrite defT defS1 (perm_catCA [::_ ; _] phi). + by rewrite defT defS1 (perm_catCA [::_; _] phi). have [c ua _ ->] := invDade_seqInd_sum (nu zeta) defT1. have def_c xi: xi \in calS -> c xi = '[xi, zeta]. move=> S2xi; rewrite /c mulrC -{1}[xi]scale1r -(mulVf nz_phi1) -!scalerA. diff --git a/mathcomp/odd_order/PFsection8.v b/mathcomp/odd_order/PFsection8.v index d4ffa46..2770369 100644 --- a/mathcomp/odd_order/PFsection8.v +++ b/mathcomp/odd_order/PFsection8.v @@ -557,7 +557,7 @@ have [part_a _ _ [part_b part_c]] := BGsummaryB maxM complU. rewrite eqEsubset FTsupp1_sub // andbT -setD_eq0 in part_c. split=> // X notX0 /subsetD1P[sXU notX1]; rewrite -cent_gen defH. apply: part_b; rewrite -?subG1 ?gen_subG //. -by rewrite -setD_eq0 setDE (setIidPl _) // subsetC sub1set inE. +by rewrite -setD_eq0 setDE (setIidPl _) // subsetC sub1set inE. Qed. (* This is Peterfalvi (8.13). *) @@ -1111,7 +1111,7 @@ without loss{suppST} suppST: T maxT ncST / FTsupports S T. have{suppST} [y /and3P[ASy not_sCyS sCyT]] := existsP suppST. have Dy: y \in [set z in 'A0(S) | ~~ ('C[z] \subset S)] by rewrite !inE ASy. have [_ [_ /(_ y Dy) uCy] /(_ y Dy)[_ coTcS _ typeT]] := FTsupport_facts maxS. -rewrite -mem_iota -(eq_uniq_mmax uCy maxT sCyT) !inE in coTcS typeT. +rewrite -mem_iota -(eq_uniq_mmax uCy maxT sCyT) !inE in coTcS typeT. apply/negbNE; rewrite -part_b /NC 1?orbit_sym // negb_exists. apply/forallP=> x; rewrite part_a1 ?mmaxJ ?negbK //; last first. by rewrite /NC (orbit_transl _ (mem_orbit _ _ _)) ?in_setT // orbit_sym. diff --git a/mathcomp/odd_order/PFsection9.v b/mathcomp/odd_order/PFsection9.v index 0cd1109..d8ec417 100644 --- a/mathcomp/odd_order/PFsection9.v +++ b/mathcomp/odd_order/PFsection9.v @@ -89,7 +89,7 @@ Let defW2 : 'C_H(W1) = W2. Proof. exact: typeP_cent_core_compl MtypeP. Qed. Lemma Ptype_Fcore_sdprod : H ><| (U <*> W1) = M. Proof. -have [_ /= sW1M mulHUW1 _ tiHUW1] := sdprod_context defM. +have [_ /= sW1M mulHUW1 _ tiHUW1] := sdprod_context defM. have [/= /andP[sHHU _] sUHU mulHU nHU tiHU] := sdprod_context defHU. rewrite sdprodE /= norm_joinEr // ?mulgA ?mulHU //. by rewrite mulG_subG nHU (subset_trans sW1M) ?gFnorm. @@ -322,7 +322,7 @@ Proof. apply: Frobenius_quotient frobUW1 _ nsCUW1 _. by apply: nilpotent_sol; have [_ []] := MtypeP. by have [] := Ptype_Fcore_factor_facts; rewrite eqEsubset sCU. -Qed. +Qed. Definition typeP_Galois := acts_irreducibly U Hbar 'Q. @@ -397,7 +397,7 @@ have [oH1 defHbar]: #|H1| = p /\ \big[dprod/1]_(w in W1bar) H1 :^ w = Hbar. by rewrite -(big_imset id injW1) -defH1W0 big_imset. split=> //; set a := #|_ : _|; pose q1 := #|(W1 / H0)^#|. have a_gt1: a > 1. - rewrite indexg_gt1 subsetIidl /= astabQ -sub_quotient_pre //. + rewrite indexg_gt1 subsetIidl /= astabQ -sub_quotient_pre //. apply: contra neqCU => cH1U; rewrite [C]unlock (sameP eqP setIidPl) /= astabQ. rewrite -sub_quotient_pre // -(bigdprodWY defHbar) cent_gen centsC. by apply/bigcupsP=> w Ww; rewrite centsC centJ -(normsP nUW1b w) ?conjSg. @@ -663,7 +663,7 @@ pose nF := <[1%R : F]>; have o_nF: #|nF| = p. have cyc_uF := @field_unit_group_cyclic F. exists F. exists phi; last first. - split=> //; first exact/isomP; apply/esym/eqP; rewrite eqEcard o_nF -phi_s. + split=> //; first exact/isomP; apply/esym/eqP; rewrite eqEcard o_nF -phi_s. by rewrite (@cycle_subG F) mem_morphim //= card_injm ?subsetIl ?oW2b. exists psi => //; last first. by split=> // h x Hh Ux; rewrite qactJ (subsetP nH0U) ?phiJ. @@ -834,7 +834,7 @@ Lemma typeP_nonGalois_characters (not_Galois : ~~ typeP_Galois) : (lb_d %| lb_n /\ lb_n %/ lb_d <= count irr_qa (S_ H0U'))%N]. Proof. case: (typeP_Galois_Pn _) => H1 [oH1 nH1U nH1Uq defHbar aP]; rewrite [sval _]/=. -move => a; case: aP; rewrite -/a => a_gt1 a_dv_p1 cycUb1 isoUb. +move=> a; case: aP; rewrite -/a => a_gt1 a_dv_p1 cycUb1 isoUb. set part_a := ({in _, _}); pose HCbar := (HC / H0)%G. have [_ /mulG_sub[sHUM sW1M] nHUW1 tiHUW1] := sdprodP defM. have [nsHHU _ /mulG_sub[sHHU sUHU] nHU tiHU] := sdprod_context defHU. @@ -870,7 +870,7 @@ have Part_a: part_a. have{kersH0} kertH0: H0 \subset cfker 'chi_t. by rewrite (sub_cfker_constt_Res_irr sHt). have Ltheta: theta \is a linear_char. - by rewrite /theta -quo_IirrE // (char_abelianP _ _). + by rewrite /theta -quo_IirrE // (char_abelianP _ _). have Dtheta : _ = theta := cfBigdprod_Res_lin defHbar Ltheta. set T := 'I_HU['chi_t]; have sHT: H \subset T by rewrite sub_Inertia. have sTHU: T \subset HU by rewrite Inertia_sub. @@ -1086,11 +1086,11 @@ split=> {Part_a part_a}//. rewrite odd_exp -(subnKC (prime_gt1 pr_q)) /= -subn1 odd_sub ?prime_gt0 //. by rewrite -oH1 (oddSg sH1H) ?quotient_odd // mFT_odd. have p1_gt0: (0 < p.-1)%N by rewrite -(subnKC (prime_gt1 p_pr)). - apply/eqP; rewrite -(eqn_pmul2r p1_gt0) -expnSr prednK ?prime_gt0 //. + apply/eqP; rewrite -(eqn_pmul2r p1_gt0) -expnSr prednK ?prime_gt0 //. by rewrite -oXtheta -defXmu card_in_imset // cardC1 card_Iirr_abelian ?oH1. clear Xmu def_IXmu Smu sSmu_mu ResIndXmu uSmu sz_Smu sz_mu s_mu_H0C Dmu. clear Mtheta Xtheta irrXtheta oXtheta sXthXH0C mu_f Fmu_f mk_mu sW1_Imu inj_mu. -clear nz_thetaH lin_thetaH lin_theta Ftheta inj_theta irr_thetaH0 def_Itheta. +clear nz_thetaH lin_thetaH lin_theta Ftheta inj_theta irr_thetaH0 def_Itheta. clear theta Dtheta => irr_qa lb_n lb_d. have sU'U: U' \subset U := der_sub 1 U. have nH0U := subset_trans sUHU nH0HU; have nH0U' := subset_trans sU'U nH0U. @@ -1157,7 +1157,7 @@ have{lam_lin} thetaH1 i j: 'Res[H1] (theta i j) = 'chi_i. have Itheta r: r \in Mtheta -> 'I_HU['chi_r]%CF = HCH1. case/imset2P=> i j; rewrite /= in_setC1 => nz_i _ Dr; apply/eqP. rewrite eqEsubset sub_Inertia //= Dr mod_IirrE // cfIirrE ?lin_char_irr //. - rewrite andbT -(quotientSGK _ (normal_sub nsH0_HCH1)) ?subIset ?nH0HU //. + rewrite andbT -(quotientSGK _ (normal_sub nsH0_HCH1)) ?subIset ?nH0HU //. rewrite inertia_mod_quo //. apply: subset_trans (sub_inertia_Res _ (nH1wHUb _ (group1 _))) _. rewrite /= conjsg1 thetaH1 (inertia_irr_prime _ p_pr) //. @@ -1533,7 +1533,7 @@ have sS10: cfConjC_subset S1 (S_ H0C'). have cohS1: coherent S1 M^# tau. apply: uniform_degree_coherence (subset_subcoherent scohS0 sS10) _. by apply: all_pred1_constant (q * a)%:R _ _; rewrite all_map filter_all. -pose S3 := filter [predC S1] (S_ H0C'); move: {2}_.+1 (ltnSn (size S3)) => nS. +pose S3 := filter [predC S1] (S_ H0C'); move: {2}_.+1 (ltnSn (size S3)) => nS. move: @S3 (sS10) (cohS1); have: {subset S1 <= S1} by []. elim: nS {-1}S1 => // nS IHnS S2 => sS12 S3 sS20 cohS2; rewrite ltnS => leS3nS. have [ntS3|] := boolP (size S3 > 0)%N; last first. @@ -1563,7 +1563,7 @@ without loss [[eqS12 irrS1 H0C_S1] [Da_p defC] [S3qu ne_qa_qu] [oS1 oS1ua]]: pose is_qu := [pred chi : 'CF(M) | chi 1%g == (q * u)%:R]. pose isn't_qu := [pred chi | is_qu chi ==> all is_qu S3]. have /hasP[chi S3chi qu'chi]: has isn't_qu S3. - rewrite /isn't_qu; have [_|] := boolP (all _ _); last by rewrite has_predC. + rewrite /isn't_qu; have [_|] := boolP (all _ _); last by rewrite has_predC. by rewrite (eq_has (fun _ => implybT _)) has_predT. have [S2'chi S0chi]: chi \notin S2 /\ chi \in S_ H0C'. by apply/andP; rewrite mem_filter in S3chi. diff --git a/mathcomp/odd_order/wielandt_fixpoint.v b/mathcomp/odd_order/wielandt_fixpoint.v index 3a9a099..e5d8ad4 100644 --- a/mathcomp/odd_order/wielandt_fixpoint.v +++ b/mathcomp/odd_order/wielandt_fixpoint.v @@ -108,7 +108,7 @@ have{B ntB sBAn tiBU} [Ku S_Ku eKu]: exists2 Ku, Ku \in S & exponent Ku == (p ^ by apply/imsetP; rewrite -MhoEabelian ?(subsetP sBAn). rewrite morphX ?(subsetP nUA) // (exponentP _ _ (mem_quotient _ Ay)) //. rewrite -sub_Ldiv -OhmEabelian ?(abelianS (Ohm_sub n _)) //=. - rewrite (OhmE n pAu) /= -(bigdprodWY defAu) genS // subsetI sub_gen //=. + rewrite (OhmE n pAu) /= -(bigdprodWY defAu) genS // subsetI sub_gen //=. apply/bigcupsP=> Ku S_Ku; rewrite sub_LdivT. have: exponent Ku %| p ^ n.+1. by rewrite (dvdn_trans (exponentS (sSAu _ S_Ku))) // -eA exponent_quotient. |