aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/ZOdiv.v
Commit message (Collapse)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
| | | | | | | | | | | | Mostly results about Zgcd (commutativity, associativity, ...). Slight improvement of ZMicromega. Beware: some lemmas of Zdiv/ Znumtheory were asking for too strict or useless hypothesis. Some minor glitches may occur. By the way, some iff lemmas about negb in Bool.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7
* A result about Zsgn(a/b), both for Zdiv and ZOdivGravatar letouzey2007-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10313 85f007b7-540e-0410-9357-904b9bb8a0f7
* First reasonably complete version of ZOdiv, including some propertiesGravatar letouzey2007-11-10
| | | | | | | | | | | that aren't so nice after all. For instance, ((a+b*c) mod c) might differ from (a mod c), due to sign issues. Minor improvements to Zdiv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10312 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 ↵Gravatar jforest2007-11-09
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* more about ZOdiv and ZOmod (still not finished)Gravatar letouzey2007-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10307 85f007b7-540e-0410-9357-904b9bb8a0f7
* setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. Gravatar letouzey2007-11-08
A file ZOdiv is added which contains results about this euclidean division. Interest compared with Zdiv: ZOdiv implements others (better?) conventions concerning negative numbers, in particular it is compatible with Caml div and mod. ZOdiv is only partially finished... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10302 85f007b7-540e-0410-9357-904b9bb8a0f7