diff options
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/Make | 2 | ||||
| -rw-r--r-- | mathcomp/character/character.v | 4 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 8 | ||||
| -rw-r--r-- | mathcomp/character/inertia.v | 6 | ||||
| -rw-r--r-- | mathcomp/character/integral_char.v | 2 | ||||
| -rw-r--r-- | mathcomp/character/mxabelem.v | 2 | ||||
| -rw-r--r-- | mathcomp/character/mxrepresentation.v | 12 |
7 files changed, 18 insertions, 18 deletions
diff --git a/mathcomp/character/Make b/mathcomp/character/Make index 43790cd..b750b49 100644 --- a/mathcomp/character/Make +++ b/mathcomp/character/Make @@ -12,6 +12,6 @@ vcharacter.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 diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index e7ea1e0..58a3688 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -1490,7 +1490,7 @@ Proof. move=> Gx; have [e [[B uB def_x] [_ e1] [-> _] _]] := repr_rsim_diag rG Gx. rewrite cfRepr1 -[n in n%:R]card_ord -sumr_const -(eq_bigr _ (in1W e1)). case/normC_sum_eq1=> [i _ | c /eqP norm_c_1 def_e]; first by rewrite e1. -have{def_e} def_e: e = const_mx c by apply/rowP=> i; rewrite mxE def_e ?andbT. +have{} def_e: e = const_mx c by apply/rowP=> i; rewrite mxE def_e ?andbT. by exists c => //; rewrite def_x def_e diag_const_mx scalar_mxC mulmxKV. Qed. @@ -1619,7 +1619,7 @@ apply: andb_id2l => Gx; rewrite {1 2}[chi]cfun_sum_constt !sum_cfunE. apply/eqP/bigcapP=> [Kx i Ci | Kx]; last first. by apply: eq_bigr => i /Kx Kx_i; rewrite !cfunE cfker1. rewrite cfkerEirr inE /= -(inj_eq (mulfI Ci)). -have:= (normC_sum_upper _ Kx) i; rewrite !cfunE => -> // {i Ci} i _. +have:= (normC_sum_upper _ Kx) i; rewrite !cfunE => -> // {Ci}i _. have chi_i_ge0: 0 <= '[chi, 'chi_i]. by rewrite Cnat_ge0 ?Cnat_cfdot_char_irr. by rewrite !cfunE normrM (normr_idP _) ?ler_wpmul2l ?char1_ge_norm ?irr_char. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index ccfc37b..2bea267 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -1093,7 +1093,7 @@ Lemma pairwise_orthogonalP S : Proof. rewrite /pairwise_orthogonal /=; case notS0: (~~ _); last by right; case. elim: S notS0 => [|phi S IH] /=; first by left. -rewrite inE eq_sym andbT => /norP[nz_phi /IH{IH}IH]. +rewrite inE eq_sym andbT => /norP[nz_phi /IH{}IH]. have [opS | not_opS] := allP; last first. right=> [[/andP[notSp _] opS]]; case: not_opS => psi Spsi /=. by rewrite opS ?mem_head 1?mem_behead // (memPnC notSp). @@ -1306,7 +1306,7 @@ Lemma isometry_of_free S f : Proof. move=> freeS If; have defS := free_span freeS. have [tau /(_ freeS (size_map f S))Dtau] := linear_of_free S (map f S). -have{Dtau} Dtau: {in S, tau =1 f}. +have{} Dtau: {in S, tau =1 f}. by move=> _ /(nthP 0)[i ltiS <-]; rewrite -!(nth_map 0 0) ?Dtau. exists tau => // _ _ /defS[a -> _] /defS[b -> _]. rewrite !{1}linear_sum !{1}cfdot_suml; apply/eq_big_seq=> xi1 Sxi1. @@ -2229,7 +2229,7 @@ rewrite (set_partition_big _ (rcosets_partition_mul H K)) ?big_imset /=. apply: eq_bigr => y Hy; rewrite rcosetE norm_rlcoset ?(subsetP nKH) //. rewrite -lcosetE mulr_natl big_imset /=; last exact: in2W (mulgI _). by rewrite -sumr_const; apply: eq_bigr => z Kz; rewrite conjgM cfunJ. -have [{nKH}nKH /isomP[injf _]] := sdprod_isom defG. +have [{}nKH /isomP[injf _]] := sdprod_isom defG. apply: can_in_inj (fun Ky => invm injf (coset K (repr Ky))) _ => y Hy. by rewrite rcosetE -val_coset ?(subsetP nKH) // coset_reprK invmE. Qed. @@ -2410,7 +2410,7 @@ Lemma map_cfAut_free S : cfAut_closed u S -> free S -> free (map (cfAut u) S). Proof. set Su := map _ S => sSuS freeS; have uniqS := free_uniq freeS. have uniqSu: uniq Su by rewrite (map_inj_uniq cfAut_inj). -have{sSuS} sSuS: {subset Su <= S} by move=> _ /mapP[phi Sphi ->]; apply: sSuS. +have{} sSuS: {subset Su <= S} by move=> _ /mapP[phi Sphi ->]; apply: sSuS. have [|_ eqSuS] := uniq_min_size uniqSu sSuS; first by rewrite size_map. by rewrite (perm_free (uniq_perm uniqSu uniqS eqSuS)). Qed. diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index 29d7162..e7f80dc 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -1140,7 +1140,7 @@ have [defKT | ltKT_K] := eqVneq (K :&: T) K; last first. by have /cfclassP[y _ ->] := mem_tnth i phiKt; rewrite cfConjg_irr ?mem_irr. constructor 3; exists p => [i j /(congr1 (tnth (irr L)))/eqP| ]. by apply: contraTeq; rewrite !pK !nth_uniq ?t_cast ?cfclass_uniq. - have{DthL} DthL: 'Res theta = e%:R *: \sum_(i < t) (phi ^: K)%CF`_i. + have{} DthL: 'Res theta = e%:R *: \sum_(i < t) (phi ^: K)%CF`_i. by rewrite DthL (big_nth 0) big_mkord t_cast. suffices /eqP e1: e == 1%N by rewrite DthL e1 scale1r; apply: eq_bigr. have Dth1: theta 1%g = e%:R * t%:R * phi 1%g. @@ -1153,7 +1153,7 @@ have [defKT | ltKT_K] := eqVneq (K :&: T) K; last first. rewrite mul1r -Dth1 -cfInd1 //. by rewrite char1_ge_constt ?cfInd_char ?irr_char ?constt_Ind_Res. have IKphi: 'I_K[phi] = K by rewrite -{1}(setIidPl sKG) -setIA. -have{DthL} DthL: 'Res[L] theta = e%:R *: phi. +have{} DthL: 'Res[L] theta = e%:R *: phi. by rewrite DthL -[rhs in (_ ^: rhs)%CF]IKphi cfclass_inertia big_seq1. pose mmLth := @mul_mod_Iirr K L s. have linKbar := char_abelianP _ abKbar. @@ -1295,7 +1295,7 @@ exists c => // c2 c2Nth det_c2_mu; apply: irr_inj. have [irrMc _ imMc _] := constt_Ind_ext nsNG chiN. have /codomP[s2 Dc2]: c2 \in codom (@mul_mod_Iirr G N c). by rewrite -imMc constt_Ind_Res c2Nth constt_irr ?inE. -have{Dc2} Dc2: 'chi_c2 = ('chi_s2 %% N)%CF * 'chi_c. +have{} Dc2: 'chi_c2 = ('chi_s2 %% N)%CF * 'chi_c. by rewrite Dc2 cfIirrE // mod_IirrE. have s2_lin: 'chi_s2 \is a linear_char. rewrite qualifE irr_char; apply/eqP/(mulIf (irr1_neq0 c)). diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index c82202b..8911134 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -376,7 +376,7 @@ rewrite ltnS => leGn piGle2; have [simpleG | ] := boolP (simple G); last first. rewrite groupP /= genGid normG andbT eqb_id negbK => /eqP->. exact: solvable1. rewrite [N == G]eqEproper sNG eqbF_neg !negbK => ltNG /and3P[grN]. - case/isgroupP: grN => {N}N -> in sNG ltNG *; rewrite /= genGid => ntN nNG. + case/isgroupP: grN => {}N -> in sNG ltNG *; rewrite /= genGid => ntN nNG. have nsNG: N <| G by apply/andP. have dv_le_pi m: (m %| #|G| -> size (primes m) <= 2)%N. move=> m_dv_G; apply: leq_trans piGle2. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 8575d58..2a9eb19 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -955,7 +955,7 @@ have rphi_fful i: mx_faithful (rphi i). have rphi_z i: rphi i z = (w ^+ i.+1)%:M. by rewrite /rphi [phi]lock /= /morphim_mx autmE alpha_i_z -lock phi_ze. pose iphi i := irr_comp sS (rphi i); pose phi_ i := irr_repr (iphi i). -have{phi_ze} phi_ze i e: phi_ i (z ^+ e)%g = (w ^+ (e * i.+1)%N)%:M. +have{} phi_ze i e: phi_ i (z ^+ e)%g = (w ^+ (e * i.+1)%N)%:M. rewrite /phi_ !{1}irr_center_scalar ?groupX ?irr_modeX //. suffices ->: irr_mode (iphi i) z = w ^+ i.+1 by rewrite mulnC exprM. have:= mx_rsim_sym (rsim_irr_comp sS F'S (rphi_irr i)). diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 6885ec7..ea93ab2 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -3114,7 +3114,7 @@ Proof. move=> addUV dxUV. have eqUV: \rank U = \rank (cokermx V). by rewrite mxrank_coker -{3}(mxrank1 F n) -addUV (mxdirectP dxUV) addnK. -have{dxUV} dxUV: (U :&: V = 0)%MS by apply/mxdirect_addsP. +have{} dxUV: (U :&: V = 0)%MS by apply/mxdirect_addsP. exists (in_submod U (val_factmod 1%:M *m proj_mx U V)) => // [|x Gx]. rewrite /row_free -{6}eqUV -[_ == _]sub1mx -val_submodS val_submod1. rewrite in_submodK ?proj_mx_sub // -{1}[U](proj_mx_id dxUV) //. @@ -3407,7 +3407,7 @@ Proof. rewrite -{9}(mxrank1 F n) -Clifford_Socle1. rewrite (mxdirectP (Socle_direct sH)) /= -sum_nat_const. apply: eq_bigr => W1 _; have [W0 _ W0G] := imsetP Clifford_atrans. -have{W0G} W0G W': W' \in orbit 'Cl G W0 by rewrite -W0G inE. +have{} W0G W': W' \in orbit 'Cl G W0 by rewrite -W0G inE. have [/orbitP[x Gx <-] /orbitP[y Gy <-]] := (W0G W, W0G W1). by rewrite !{1}val_Clifford_act // !mxrankMfree // !repr_mx_free. Qed. @@ -4299,7 +4299,7 @@ have simM: mxsimple aG M. rewrite (eqmx_module _ (genmxE _)); apply/mxmoduleP=> x Gx. by rewrite -mulmxA -homf // mulmxA submxMr // (mxmoduleP modU). pose i := PackSocle (component_socle sG simM). -have{modM rsimM} rsimM: mx_rsim rG (socle_repr i). +have{modM} rsimM: mx_rsim rG (socle_repr i). apply: mx_rsim_trans rsimM (mx_rsim_sym _); apply/mx_rsim_iso. apply: (component_mx_iso (socle_simple _)) => //. by rewrite [component_mx _ _]PackSocleK component_mx_id. @@ -4812,7 +4812,7 @@ Lemma dec_mx_reducible_semisimple U : Proof. have [m] := ubnP (\rank U); elim: m U => // m IHm U leUm modU redU. have [U0 | nzU] := eqVneq U 0. - have{U0} U0: (\sum_(i < 0) 0 :=: U)%MS by rewrite big_ord0 U0. + have{} U0: (\sum_(i < 0) 0 :=: U)%MS by rewrite big_ord0 U0. by apply: (intro_mxsemisimple U0); case. have [V simV sVU] := dec_mxsimple_exists modU nzU; have [modV nzV _] := simV. have [W modW defVW dxVW] := redU V modV sVU. @@ -5035,7 +5035,7 @@ have compUf: mx_composition_series (regular_repr rF G) Uf. rewrite -{2}(map_mx0 f) -map_cons !(nth_map 0) ?leqW //. by rewrite map_submx // ltmxW // (pathP _ (mx_series_lt compU)). have [[i ltiU] simUi] := rsim_regular_series irrG compUf lastUf. -have{simUi} simUi: mx_rsim rG (subseries_repr i modUf). +have{} simUi: mx_rsim rG (subseries_repr i modUf). by apply: mx_rsim_trans simUi _; apply: section_eqmx. by rewrite (mx_rsim_abs_irr simUi) absUf; rewrite size_map in ltiU. Qed. @@ -5693,7 +5693,7 @@ elim: t => //=. - move=> t1 IH1 n1 rt1; rewrite eval_mulmx eval_mx_term mul_scalar_mx. by rewrite scaler_nat {}IH1 //; elim: n1 => //= n1 IHn1; rewrite !mulrS IHn1. - by move=> t1 IH1 t2 IH2 /andP[rt1 rt2]; rewrite eval_mulT IH1 ?IH2. -move=> t1 IH1 n1 /IH1 {IH1}IH1. +move=> t1 + n1 => /[apply] IH1. elim: n1 => [|n1 IHn1] /=; first by rewrite eval_mx_term. by rewrite eval_mulT exprS IH1 IHn1. Qed. |