diff options
| author | Cyril Cohen | 2018-12-13 15:05:06 +0100 |
|---|---|---|
| committer | GitHub | 2018-12-13 15:05:06 +0100 |
| commit | f962d2a88254a99bffbc7d0a40949872a80f4669 (patch) | |
| tree | 60a84ff296299226d530dd0b495be24fd7675748 /mathcomp/algebra/intdiv.v | |
| parent | fa9b7b19fc0409f3fdfa680e08f40a84594e8307 (diff) | |
| parent | 0b1ea03dafcf36880657ba910eec28ab78ccd018 (diff) | |
Merge pull request #262 from math-comp/cancel-lemmas-implicit
Cancel lemmas implicit
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. |