From e565f8d9bebd4fd681c34086d5448dbaebc11976 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 19 Nov 2020 18:33:21 +0100 Subject: Removing duplicate clears and turning the warning into an error --- mathcomp/solvable/Make | 2 +- mathcomp/solvable/abelian.v | 2 +- mathcomp/solvable/alt.v | 2 +- mathcomp/solvable/extraspecial.v | 2 +- mathcomp/solvable/extremal.v | 10 +++++----- mathcomp/solvable/maximal.v | 6 +++--- mathcomp/solvable/nilpotent.v | 2 +- mathcomp/solvable/primitive_action.v | 2 +- mathcomp/solvable/sylow.v | 4 ++-- 9 files changed, 16 insertions(+), 16 deletions(-) (limited to 'mathcomp/solvable') diff --git a/mathcomp/solvable/Make b/mathcomp/solvable/Make index fd00057..2f5aac3 100644 --- a/mathcomp/solvable/Make +++ b/mathcomp/solvable/Make @@ -24,6 +24,6 @@ sylow.v -arg -w -arg -projection-no-head-constant -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden --arg -w -arg -duplicate-clear +-arg -w -arg +duplicate-clear -arg -w -arg -ambiguous-paths -arg -w -arg +undeclared-scope \ No newline at end of file diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index ba26ab6..2163b7d 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -299,7 +299,7 @@ rewrite partn_dvd ?exponentS ?exponent_gt0 //=; apply/dvdn_partP=> // p. rewrite pi_of_part ?exponent_gt0 // => /andP[_ /= pi_p]. have sppi: {subset (p : nat_pred) <= pi} by move=> q /eqnP->. have [P sylP] := Sylow_exists p H; have sPH := pHall_sub sylP. -have{sylP} sylP: p.-Sylow(G) P. +have{} sylP: p.-Sylow(G) P. rewrite pHallE (subset_trans sPH) //= (card_Hall sylP) eqn_dvd andbC. by rewrite -{1}(partn_part _ sppi) !partn_dvd ?cardSg ?cardG_gt0. rewrite partn_part ?partn_biglcm //. diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index e67a0f9..f95069a 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.v @@ -270,7 +270,7 @@ have nSyl5: #|'Syl_5(H)| = 1%N. move: (dvdn_leq (isT: (0 < 20)%N) Hdiv). by move: (n) Hdiv; do 20 (case=> //). case: (Sylow_exists 5 H) => S; case/pHallP=> sSH oS. -have{oS} oS: #|S| = 5 by rewrite oS p_part Hcard20. +have{} oS: #|S| = 5 by rewrite oS p_part Hcard20. suff: 20 %| #|S| by rewrite oS. apply: FF => [|S1]; last by rewrite S1 cards1 in oS. apply: char_normal_trans Hnorm; apply: lone_subgroup_char => // Q sQH isoQS. diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index 2dcb1d5..6d1a01f 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -538,7 +538,7 @@ elim: Es {+}G => [|E Es IHs] S in n oG expG p3Es defG *. by rewrite isog_cyclic_card prime_cyclic ?oZ ?card_pX1p2n //=. rewrite big_cons -cprodA in defG; rewrite /= -andbA in p3Es. have [[_ T _ defT] defET cTE] := cprodP defG; rewrite defT in defET cTE defG. -case/and3P: p3Es; move/eqP=> oE; move/eqP=> defZE; move/IHs=> {IHs}IHs. +move: p3Es => /and3P[/eqP oE /eqP defZE /IHs{}IHs]. have not_cEE: ~~ abelian E. by apply: contra not_le_p3_p => cEE; rewrite -oE -oZ -defZE (center_idP _). have sES: E \subset S by rewrite -defET mulG_subl. diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index a0c40ee..8e6e002 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -862,7 +862,7 @@ Proof. move=> n_gt1; have [def2q _ ltqm _] := def2qr n_gt1. case/(isoGrpP _ (Grp_2dihedral n_gt1)); rewrite card_2dihedral // -/ m => oG. case/existsP=> -[x y] /=; rewrite -/q => /eqP[defG xq y2 xy]. -have{defG} defG: <[x]> * <[y]> = G. +have{} defG: <[x]> * <[y]> = G. by rewrite -norm_joinEr // norms_cycle xy groupV cycle_id. have notXy: y \notin <[x]>. apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //. @@ -884,7 +884,7 @@ move=> n_gt3; have [def2q _ ltqm _] := def2qr (ltnW (ltnW n_gt3)). case/(isoGrpP _ (Grp_semidihedral n_gt3)). rewrite card_semidihedral // -/m => oG. case/existsP=> -[x y] /=; rewrite -/q -/r => /eqP[defG xq y2 xy]. -have{defG} defG: <[x]> * <[y]> = G. +have{} defG: <[x]> * <[y]> = G. by rewrite -norm_joinEr // norms_cycle xy mem_cycle. have notXy: y \notin <[x]>. apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //. @@ -905,7 +905,7 @@ Proof. move=> n_gt2; have [def2q def2r ltqm _] := def2qr (ltnW n_gt2). case/(isoGrpP _ (Grp_quaternion n_gt2)); rewrite card_quaternion // -/m => oG. case/existsP=> -[x y] /=; rewrite -/q -/r => /eqP[defG xq y2 xy]. -have{defG} defG: <[x]> * <[y]> = G. +have{} defG: <[x]> * <[y]> = G. by rewrite -norm_joinEr // norms_cycle xy groupV cycle_id. have notXy: y \notin <[x]>. apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //. @@ -1949,7 +1949,7 @@ have [a [fGa oa au n_gt01 cycGs]]: exists a, rewrite -(injm_p_rank injf) // p_rank_abelian 1?morphim_abelian //= p2 -/Gs. case: leqP => [|fGs1_gt1]; [by left | right]. split=> //; exists c; last by rewrite -def_m // m_c expg_zneg. - have{defA1} defA1: <[a]> \x <[c]> = 'Ohm_1(Aut U). + have{} defA1: <[a]> \x <[c]> = 'Ohm_1(Aut U). by rewrite -(Ohm_dprod 1 defA) defA1 (@Ohm_p_cycle 1 _ 2) /p_elt oc. have def_fGs1: 'Ohm_1(f @* Gs) = 'Ohm_1(A). apply/eqP; rewrite eqEcard OhmS // -(dprod_card defA1) -!orderE oa oc. @@ -2240,7 +2240,7 @@ have tiER: E :&: R = 'Z(E) by rewrite setIA (setIidPl (subset_trans sEH sHG)). have [cRR | not_cRR] := boolP (abelian R). exists E; [by right | exists [group of R]; split=> //; left]. by rewrite /= -(setIidPl (sub_abelian_cent cRR sUR)) scUR. -have{scUR} scUR: [group of U] \in 'SCN(R). +have{} scUR: [group of U] \in 'SCN(R). by apply/SCN_P; rewrite (normalS sUR (subsetIl _ _)) // char_normal. have pR: p.-group R := pgroupS (subsetIl _ _) pG. have [R_le_3 | R_gt_3] := leqP (logn p #|R|) 3. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index af0001c..7f36723 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1216,8 +1216,8 @@ set T := S; exists (logn p #|T|)./2. have [Es] := extraspecial_structure pS esS; rewrite -[in RHS]/T. elim: Es T => [_ _ <-| E s IHs T] /=. by rewrite big_nil cprod1g oZ (pfactorK 1). -rewrite -andbA big_cons -cprodA; case/and3P; move/eqP=> oEp3; move/eqP=> defZE. -move/IHs=> {IHs}IHs; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU. +rewrite -andbA big_cons -cprodA => /and3P[/eqP oEp3 /eqP defZE]. +move=> /IHs{}IHs /cprodP[[_ U _ defU]]; rewrite defU => defT cEU. rewrite -(mulnK #|T| (cardG_gt0 (E :&: U))) -defT -mul_cardG /=. have ->: E :&: U = 'Z(S). apply/eqP; rewrite eqEsubset subsetI -{1 2}defZE subsetIl setIS //=. @@ -1385,7 +1385,7 @@ have{CAx GAx}: <[coset A x]> <| G / A. by rewrite /normal cycle_subG GAx cents_norm // centsC cycle_subG. case/(inv_quotientN nsAG)=> B /= defB sAB nBG. rewrite -cycle_subG defB (maxA B) ?trivg_quotient // nBG. -have{defB} defB : B :=: A * <[x]>. +have{} defB : B :=: A * <[x]>. rewrite -quotientK ?cycle_subG ?quotient_cycle // defB quotientGK //. exact: normalS (normal_sub nBG) nsAG. apply/setIidPl; rewrite ?defB -[_ :&: _]center_prod //=. diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index 06f3152..cf6503a 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -424,7 +424,7 @@ have <-: 'Z(H / Z) * 'Z(K / Z) = 'Z(G / Z). by rewrite -mulHK quotientMl // center_prod ?quotient_cents. have ZquoZ (B A : {group gT}): B \subset 'C(A) -> 'Z_n(A) * 'Z_n(B) = Z -> 'Z(A / Z) = 'Z_n.+1(A) / Z. -- move=> cAB {defZ}defZ; have cAZnB: 'Z_n(B) \subset 'C(A) := gFsub_trans _ cAB. +- move=> cAB {}defZ; have cAZnB: 'Z_n(B) \subset 'C(A) := gFsub_trans _ cAB. have /second_isom[/=]: A \subset 'N(Z). by rewrite -defZ normsM ?gFnorm ?cents_norm // centsC. suffices ->: Z :&: A = 'Z_n(A). diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index 80005a4..27c0780 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -120,7 +120,7 @@ have [trG _] := andP primG; have [x Sx defS] := imsetP trG. move: primG; rewrite (trans_prim_astab Sx) // => /maximal_eqP[_]. case/(_ ('C_G[x | to] <*> H)%G) => /= [||cxH|]; first exact: joing_subl. - by rewrite join_subG subsetIl. -- have{cxH} cxH: H \subset 'C_G[x | to] by rewrite -cxH joing_subr. +- have{} cxH: H \subset 'C_G[x | to] by rewrite -cxH joing_subr. rewrite subsetI sHG /= in cxH; left; apply/subsetP=> a Ha. apply/astabP=> y Sy; have [b Gb ->] := atransP2 trG Sx Sy. rewrite actCJV [to x (a ^ _)](astab1P _) ?(subsetP cxH) //. diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index fcbe7e8..3d2685b 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -148,7 +148,7 @@ have sylP: p.-Sylow(G) P. by rewrite p'natE // -indexgI -oSiN // /dvdn oS1. have eqS Q: maxp G Q = p.-Sylow(G) Q. apply/idP/idP=> [S_Q|]; last exact: Hall_max. - have{S_Q} S_Q: Q \in S by rewrite inE. + have{} S_Q: Q \in S by rewrite inE. rewrite pHallE -(card_Hall sylP); case: (S_pG Q) => // -> _ /=. by case: (atransP2 trS S_P S_Q) => x _ ->; rewrite cardJg. have ->: 'Syl_p(G) = S by apply/setP=> Q; rewrite 2!inE. @@ -568,7 +568,7 @@ Theorem Baer_Suzuki x G : x \in 'O_p(G). Proof. have [n] := ubnP #|G|; elim: n G x => // n IHn G x /ltnSE-leGn Gx pE. -set E := x ^: G; have{pE} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}. +set E := x ^: G; have{} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}. move=> _ _ /imsetP[y1 Gy1 ->] /imsetP[y2 Gy2 ->]. rewrite -(mulgKV y1 y2) conjgM -2!conjg_set1 -conjUg genJ pgroupJ. by rewrite pE // groupMl ?groupV. -- cgit v1.2.3