diff options
| author | Cyril Cohen | 2019-03-26 13:48:38 +0100 |
|---|---|---|
| committer | GitHub | 2019-03-26 13:48:38 +0100 |
| commit | 5c5455be722fe60634f511c876e05e3201091e25 (patch) | |
| tree | f9cbe81a565d7d9634bcb4a84ffcb572986cd6d9 /mathcomp/character | |
| parent | 07f9f2b983f4e61d4dc930146d3823b485f35b91 (diff) | |
| parent | 9c8f15339e719321d1a04360d3d2052ecd8bb5a2 (diff) | |
Merge pull request #305 from CohenCyril/sumn
compat sumn with bigop
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/mxabelem.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 1d8f785..65f06c4 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -897,7 +897,7 @@ have nb_irr: #|sS| = (p ^ n.*2 + p.-1)%N. rewrite ((_ ^: _ =P [set x ^ y])%g _) ?sub1set // eq_sym eqEcard. rewrite sub1set class_refl cards1 -index_cent1 (setIidPl _) ?indexgg //. by rewrite sub_cent1; apply: subsetP Zxy; apply: subsetIr. - rewrite sum_nat_dep_const mulnC eqn_pmul2l //; move/eqP <-. + rewrite sum_nat_cond_const mulnC eqn_pmul2l //; move/eqP <-. rewrite addSnnS prednK // -cardZcl -[card _](cardsID Zcl) /= addnC. by congr (_ + _)%N; apply: eq_card => t; rewrite !inE andbC // andbAC andbb. have fful_nlin i: i \in ~: linS -> mx_faithful (irr_repr i). |