diff options
| author | Cyril Cohen | 2019-03-20 18:31:45 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-03-24 00:04:29 +0100 |
| commit | 9c8f15339e719321d1a04360d3d2052ecd8bb5a2 (patch) | |
| tree | fc3fdae51954678506ab64575e1ef33eb8485525 /mathcomp/character/mxabelem.v | |
| parent | 794cfe568c2b2e1eb138a8f881c330838d8a3c2d (diff) | |
Compat of sumn with bigop and renaming dep to cond when appropriate
Diffstat (limited to 'mathcomp/character/mxabelem.v')
| -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). |