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/algebra/polyXY.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/algebra/polyXY.v')

diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v
index 5a84da7..fe0acb4 100644
--- a/mathcomp/algebra/polyXY.v
+++ b/mathcomp/algebra/polyXY.v
@@ -136,7 +136,7 @@ Qed.
 Lemma max_size_evalC u x : size u.[x%:P] <= sizeY u.
 Proof.
 rewrite horner_coef (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP=> i _.
-rewrite (leq_trans (size_mul_leq _ _)) // -polyCX size_polyC addnC -subn1.
+rewrite (leq_trans (size_mul_leq _ _)) // -polyC_exp size_polyC addnC -subn1.
 by rewrite (leq_trans _ (max_size_coefXY _ i)) // leq_subLR leq_add2r leq_b1.
 Qed.
 
@@ -192,7 +192,7 @@ Lemma horner_swapXY u x : (swapXY u).[x%:P] = u ^ eval x.
 Proof.
 apply/polyP=> i /=; rewrite coef_map /= /eval horner_coef coef_sum -sizeYE.
 rewrite (horner_coef_wide _ (max_size_coefXY u i)); apply: eq_bigr=> j _.
-by rewrite -polyCX coefMC coef_swapXY.
+by rewrite -polyC_exp coefMC coef_swapXY.
 Qed.
 
 Lemma horner_polyC u x : u.[x%:P] = swapXY u ^ eval x.
-- 
cgit v1.2.3