diff options
| author | Kazuhiko Sakaguchi | 2020-10-29 12:29:08 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-10-29 12:31:31 +0900 |
| commit | 8be036afb4445cdc009bfb244fbf593dacbe95b7 (patch) | |
| tree | ae7704d9dc0249f975d7380f997e0a8210d0d4fd /mathcomp/algebra | |
| parent | c6e0d703165b0c60c270672eb542aa8934929bfe (diff) | |
Add `dvdpNl` and rename `dvdpN` to `dvdpNr`
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index ebb8a5b..356b8ae 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -1434,7 +1434,12 @@ Proof. by move=> cn0; exact/eqp_dvdr/eqp_scale. Qed. Lemma dvdpZl c m n : c != 0 -> (c *: m %| n) = (m %| n). Proof. by move=> cn0; exact/eqp_dvdl/eqp_scale. Qed. -Lemma dvdpN d p : d %| (- p) = (d %| p). +Lemma dvdpNl d p : (- d) %| p = (d %| p). +Proof. +by rewrite -scaleN1r; apply/eqp_dvdl/eqp_scale; rewrite oppr_eq0 oner_neq0. +Qed. + +Lemma dvdpNr d p : d %| (- p) = (d %| p). Proof. by apply: eqp_dvdr; rewrite -scaleN1r eqp_scale ?oppr_eq0 ?oner_eq0. Qed. Lemma eqp_mul2r r p q : r != 0 -> (p * r %= q * r) = (p %= q). @@ -2358,7 +2363,7 @@ Notation "@ 'dvdp_scalel'" := Notation "@ 'dvdp_scaler'" := (deprecate dvdp_scaler dvdpZr) (at level 10, only parsing) : fun_scope. Notation "@ 'dvdp_opp'" := - (deprecate dvdp_opp dvdpN) (at level 10, only parsing) : fun_scope. + (deprecate dvdp_opp dvdpNr) (at level 10, only parsing) : fun_scope. Notation "@ 'coprimep_scalel'" := (deprecate coprimep_scalel coprimepZl) (at level 10, only parsing) : fun_scope. Notation "@ 'coprimep_scaler'" := |