diff options
| author | Kazuhiko Sakaguchi | 2020-10-09 00:21:00 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-10-29 12:31:31 +0900 |
| commit | c6e0d703165b0c60c270672eb542aa8934929bfe (patch) | |
| tree | 3ce1b05b861ca60e88bc7ab8b5226b12a879e3e6 /mathcomp/algebra/polyXY.v | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
Switch from long suffixes to short suffixes
Diffstat (limited to 'mathcomp/algebra/polyXY.v')
| -rw-r--r-- | mathcomp/algebra/polyXY.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |