From 9c8f15339e719321d1a04360d3d2052ecd8bb5a2 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 20 Mar 2019 18:31:45 +0100
Subject: Compat of sumn with bigop and renaming dep to cond when appropriate

---
 mathcomp/character/mxabelem.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/character')

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).
-- 
cgit v1.2.3