aboutsummaryrefslogtreecommitdiff
path: root/src/WeierstrassCurve/Pre.v
Commit message (Expand)AuthorAge
* rename-everythingGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* address some code review commentsGravatar Andres Erbsen2017-03-02
* Weierstrass curve is a groupGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* remove eq_dec from MonoidGravatar Andres Erbsen2016-08-23
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* Move most notation level declarations into UtilGravatar Jason Gross2016-07-27
* remove field_algebraGravatar Andres Erbsen2016-07-11
* port CompleteEdwardsCurveTheorems (builds again)Gravatar Andres Erbsen2016-07-11
* Define the spec of Weierstrass curves (#6)Gravatar Jason Gross2016-07-03