From bd02346e4038871f4d4021dd84df384fc8cf9aa4 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 30 Oct 2020 12:12:26 +0900
Subject: Use `exp` rather than `X` for exponents of polynomials

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

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v
index 0512767..e51a660 100644
--- a/mathcomp/field/separable.v
+++ b/mathcomp/field/separable.v
@@ -625,7 +625,7 @@ have [K'g]: g \is a polyOver K' /\ q \is a polyOver K'.
 have /dvdpP[c Dq]: 'X - x%:P %| q by rewrite dvdp_XsubCl root_minPoly.
 have co_c_g: coprimep c g.
   have charPp: p \in [char {poly L}] := rmorph_char (polyC_rmorphism _) charLp.
-  rewrite /g polyCX -!(Frobenius_autE charPp) -rmorphB coprimepXr //.
+  rewrite /g polyC_exp -!(Frobenius_autE charPp) -rmorphB coprimep_expr //.
   have: separable_poly q := separable_elementS sKK' sepKx.
   by rewrite Dq separable_mul => /and3P[].
 have{g K'g co_c_g} /size_poly1P[a nz_a Dc]: size c == 1%N.
-- 
cgit v1.2.3