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/algebra/polyXY.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mathcomp/algebra/polyXY.v') diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index 9bc8fd5..5a84da7 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 _ _)) // -polyC_exp size_polyC addnC -subn1. +rewrite (leq_trans (size_mul_leq _ _)) // -polyCX 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 -polyC_exp coefMC coef_swapXY. +by rewrite -polyCX coefMC coef_swapXY. Qed. Lemma horner_polyC u x : u.[x%:P] = swapXY u ^ eval x. @@ -228,7 +228,7 @@ Proof. by rewrite -!size_poly_eq0 size_poly_XmY. Qed. Lemma lead_coef_poly_XaY p : lead_coef (poly_XaY p) = (lead_coef p)%:P. Proof. -rewrite lead_coef_comp ?size_XaddC // -['Y]opprK -polyC_opp lead_coefXsubC. +rewrite lead_coef_comp ?size_XaddC // -['Y]opprK -polyCN lead_coefXsubC. by rewrite expr1n mulr1 lead_coef_map_inj //; apply: polyC_inj. Qed. -- cgit v1.2.3 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