aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/PrimeFieldTheorems.v
Commit message (Expand)AuthorAge
* proved most of point encoding admits, fixed some build system issues (dead im...Gravatar Jade Philipoom2016-02-16
* moved two non-primality-dependent lemmas to ModularArithmeticTheorems from Pr...Gravatar Jade Philipoom2016-02-15
* Merge branch 'spec' of github.mit.edu:plv/fiat-crypto into specGravatar Jade Philipoom2016-02-15
|\
* | added square roots and an assortment of lemmas about prime fields/ringsGravatar Jade Philipoom2016-02-15
|/
* prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd Cl...Gravatar Andres Erbsen2016-02-13
* port some edwards curve theoremsGravatar Andres Erbsen2016-02-12
* port some Edwards curve stuff from GF to FGravatar Andres Erbsen2016-02-11
* port several theorems from GF to FGravatar Andres Erbsen2016-02-11
* Define F m, a replacement for GF with several benefits.Gravatar Andres Erbsen2016-02-11