aboutsummaryrefslogtreecommitdiff
path: root/src/Util/NumTheoryUtil.v
Commit message (Expand)AuthorAge
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* coqprime in COQPATH (closes #269)Gravatar Andres Erbsen2018-02-24
* NumTheoryUtil: make coqprime dependencies explicitGravatar Andres Erbsen2018-02-19
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* do not use VerdiTactics in files we plan to keepGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* address code review commentsGravatar Andres Erbsen2016-08-04
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* Make ZUtil more uniformGravatar Jason Gross2016-07-02
* Finish absolutizing importsGravatar Jason Gross2016-03-10
* tweak to NumTheoryUtil so it builds on older Coq versionsGravatar Jade Philipoom2016-03-03
* ModularArithmetic: reasonable-time FieldToZ inv implementationGravatar Andres Erbsen2016-02-26
* tweaks to util files, including automation for proving positivity/nonnegativi...Gravatar Jade Philipoom2016-02-15
* GaloisTheory: added lemmas useful for proving Euler's Criterion with GF. NumT...Gravatar Jade Philipoom2016-02-02
* NumTheoryUtil: proved Fermat's Little Theorem.Gravatar Jade Philipoom2016-01-23
* NumTheoryUtil : code cleanup; moved some lemmas to ZUtil.Gravatar Jade Philipoom2016-01-23
* Import coqprime; use it to prove Euler's criterion.Gravatar Jade Philipoom2016-01-20
* euler's criterion reduced to fermat's little theorem and two lemmas about pri...Gravatar Jade Philipoom2016-01-13
* Util: added util lemmas needed to instantiate EdDSA25519.Gravatar Jade Philipoom2016-01-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 23:04:45 +0000