diff options
Diffstat (limited to 'mathcomp/algebra/intdiv.v')
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 2f5e844..1da8313 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -714,7 +714,7 @@ rewrite mul1n; apply/dvdn_biggcdP/(all_nthP 0)=> a_dv_p i ltip /=. exact: a_dv_p. Qed. -Lemma map_poly_divzK a p : +Lemma map_poly_divzK {a} p : p \is a polyOver (dvdz a) -> a *: map_poly (divz^~ a) p = p. Proof. move/polyOverP=> a_dv_p; apply/polyP=> i. |