diff options
Diffstat (limited to 'mathcomp/algebra/polyXY.v')
| -rw-r--r-- | mathcomp/algebra/polyXY.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index 9bc8fd5..fe0acb4 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.v @@ -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. |