aboutsummaryrefslogtreecommitdiff
path: root/src/Util/NumTheoryUtil.v
Commit message (Expand)AuthorAge
* 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-05-04 11:21:41 +0000