diff options
| author | Kazuhiko Sakaguchi | 2020-10-30 12:12:26 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-10-30 12:12:26 +0900 |
| commit | bd02346e4038871f4d4021dd84df384fc8cf9aa4 (patch) | |
| tree | 62f0dc367dc9ab3fa4210ee5e003b03a34eda25f /mathcomp/algebra/polyXY.v | |
| parent | a9767fcd4713fc37e57fc9cc2a7864879effbf73 (diff) | |
Use `exp` rather than `X` for exponents of polynomials
Diffstat (limited to 'mathcomp/algebra/polyXY.v')
| -rw-r--r-- | mathcomp/algebra/polyXY.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |