From c6e0d703165b0c60c270672eb542aa8934929bfe Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 9 Oct 2020 00:21:00 +0900
Subject: Switch from long suffixes to short suffixes

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

(limited to 'mathcomp/character/mxabelem.v')

diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index 92470d9..949ded3 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -469,7 +469,7 @@ Local Notation rVn := 'rV['F_p](gval E).
 Lemma dim_abelemE : n = logn p #|E|.
 Proof.
 rewrite /n'; have [_ _ [k ->]] :=  pgroup_pdiv pE ntE.
-by rewrite /pdiv primes_exp ?primes_prime // pfactorK.
+by rewrite /pdiv primesX ?primes_prime // pfactorK.
 Qed.
 
 Lemma card_abelem_rV : #|rVn| = #|E|.
-- 
cgit v1.2.3