diff options
Diffstat (limited to 'mathcomp/algebra/intdiv.v')
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 4c5ad4d..933bfcb 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -340,14 +340,14 @@ apply: (iffP dvdnP) => [] [q Dm]; last by exists `|q|%N; rewrite Dm abszM. exists ((-1) ^+ (m < 0)%R * q%:Z * (-1) ^+ (d < 0)%R). by rewrite -!mulrA -abszEsign -PoszM -Dm -intEsign. Qed. -Arguments dvdzP [d m]. +Arguments dvdzP {d m}. Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z. Proof. apply: (iffP dvdzP) => [[q ->] | md0]; first by rewrite modzMl. by rewrite (divz_eq m d) md0 addr0; exists (m %/ d)%Z. Qed. -Arguments dvdz_mod0P [d m]. +Arguments dvdz_mod0P {d m}. Lemma dvdz_eq d m : (d %| m)%Z = ((m %/ d)%Z * d == m). Proof. by rewrite (sameP dvdz_mod0P eqP) subr_eq0 eq_sym. Qed. |